1 /-
2 Copyright (c) 2018 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir
5 -/
6 import algebra.archimedean algebra.geom_sum
src └─────────────────┘ └──────────────┘
7 import data.nat.choose data.complex.basic
src └─────────────┘ └────────────────┘
8 import tactic.linarith
src └─────────────┘
9
10 local notation `abs'` := _root_.abs
id └────────┘
src └────────┘
typ └────────┘
11 open is_absolute_value
12 open_locale classical
13
14 section
15 open real is_absolute_value finset
16
17 lemma forall_ge_le_of_forall_le_succ {α : Type*} [preorder α] (f : ℕ → α) {m : ℕ}
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴
18 (h : ∀ n ≥ m, f n.succ ≤ f n) : ∀ {l}, ∀ k ≥ m, k ≤ l → f l ≤ f k :=
id ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
19 begin
st └─────
20 assume l k hkm hkl,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ───────────────────┘└─
21 generalize hp : l - k = p,
id ┴ ┴ ┴
src └──────────────┘ ┴┴┴ ┴ ┴
typ └──────────────┘┴┴┴┴┴┴ ┴
doc └──────────────┘ ┴ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ ┴ ┴
pid └─┘└┘┴ ┴ ┴ ┴ ┴
st ──────────────────────────┘└─
22 have : l = k + p := add_comm p k ▸ (nat.sub_eq_iff_eq_add hkl).1 hp,
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └───────────────────┘ └─┘ └┘
src └─────┘ ┴ ┴ ┴┴┴ └──┘└──────┘┴ ┴ ┴┴┴ └───────────────────┘┴ └──┘
typ └─────┘┴┴ ┴┴┴┴┴┴└──┘└──────┘┴┴┴┴┴┴┴ └───────────────────┘┴└─┘└──┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────┘└─
23 subst this,
id └──┘
src └────┘
typ └────┘└──┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
24 clear hkl hp,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └─────┘
st ─────────────┘└─
25 induction p with p ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
26 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
27 { exact le_trans (h _ (le_trans hkm (nat.le_add_right _ _))) ih }
id ┴ └──────┘ └─┘ └──────────────┘ └┘
src └────┘ ┴ └─┘ └──────┘┴ ┴ └──────────────┘└──────┘ ┴
typ └────┘ ┴ ┴└─┘ └──────┘┴└─┘┴ └──────────────┘└──────┘└┘┴
doc └────┘ ┴ └─┘ ┴ ┴ └──────┘ ┴
txt └────┘ ┴ └─┘ ┴ ┴ └──────┘ ┴
par └────┘ ┴ └─┘ ┴ ┴ └──────┘ ┴
pid ┴ ┴ └─┘ ┴ ┴ └──────┘ ┴
st ─────────────────────────────────────────────────────────────────┘└─
28 end
st ──┘
29
30 variables {α : Type*} {β : Type*} [ring β]
id ┴ ┴ └──┘
src └──┘
typ ┴ ┴ └──┘
31 [discrete_linear_ordered_field α] [archimedean α] {abv : β → α} [is_absolute_value abv]
id └───────────────────────────┘ └─────────┘ └───────────────┘
src └───────────────────────────┘ └─────────┘ └───────────────┘
typ └───────────────────────────┘ └─────────┘ └───────────────┘
doc └───────────────┘
32
33 lemma is_cau_of_decreasing_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, abs (f n) ≤ a)
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
34 (hnm : ∀ n ≥ m, f n.succ ≤ f n) : is_cau_seq abs f :=
id ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └────────┘ └─┘ ┴
src └───┘ ┴ └────────┘ └─┘
typ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └────────┘ └─┘ ┴
doc └────────┘
35 λ ε ε0,
id ┴ └┘
typ ┴ └┘
36 let ⟨k, hk⟩ := archimedean.arch a ε0 in
id └─┘ ┴ └──────────────┘ ┴ └┘
src └──────────────┘
typ └─┘ ┴ └──────────────┘ ┴ └┘
37 have h : ∃ l, ∀ n ≥ m, a - add_monoid.smul l ε < f n :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─────────────┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
38 ⟨k + k + 1, λ n hnm, lt_of_lt_of_le
id ┴ ┴ ┴ └─┘ └────────────┘
src ┴ ┴ └────────────┘
typ ┴ ┴ ┴ └─┘ └────────────┘
39 (show a - add_monoid.smul (k + (k + 1)) ε < -abs (f n),
id ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴
src ┴ └─────────────┘ ┴ ┴ ┴ ┴└─┘
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴
40 from lt_neg.1 $ lt_of_le_of_lt (ham n hnm) (begin
id └────┘┴ └────────────┘ └─┘ ┴ └─┘
src └────┘┴ └────────────┘
typ └────┘┴ └────────────┘ └─┘ ┴ └─┘
st └─────
41 rw [neg_sub, lt_sub_iff_add_lt, add_monoid.add_smul],
id └─────┘ └───────────────┘ └─────────────────┘
src └──┘└─────┘└┘└───────────────┘└┘└─────────────────┘┴
typ └──┘└─────┘└┘└───────────────┘└┘└─────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────┘└─────────────────┘└───────────────────┘└──
42 exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk
id └────────────────────┘ └────────────┘ └┘
src └────┘└────────────────────┘┴ ┴ └────────────┘┴ └
typ └────┘└────────────────────┘┴ ┴ └────────────┘┴└┘└
doc └────┘ ┴ ┴ ┴ └
txt └────┘ ┴ ┴ ┴ └
par └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────────
43 (lt_add_of_pos_left _ ε0)),
id └────────────────┘ └┘
src ─────────┘ └────────────────┘└─┘ └┘
typ ─────────┘ └────────────────┘└─┘└┘└┘
doc ─────────┘ └─┘ └┘
txt ─────────┘ └─┘ └┘
par ─────────┘ └─┘ └┘
pid ─────────┘ └─┘ └┘
st ───────────────────────────────────┘└─
44 end))
st ────────┘
45 (neg_le.2 $ (abs_neg (f n)) ▸ le_abs_self _)⟩,
id └────┘┴ └─────┘ ┴ ┴ ┴ └─────────┘
src └────┘┴ └─────┘ ┴ └─────────┘
typ └────┘┴ └─────┘ ┴ ┴ ┴ └─────────┘
46 let l := nat.find h in
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
47 have hl : ∀ (n : ℕ), n ≥ m → f n > a - add_monoid.smul l ε := nat.find_spec h,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └───────────┘ ┴
src ┴ ┴ ┴ ┴ └─────────────┘ └───────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ └───────────┘ ┴
48 have hl0 : l ≠ 0 := λ hl0, not_lt_of_ge (ham m (le_refl _))
id ┴ ┴ └─┘ └──────────┘ └─┘ ┴ └─────┘
src ┴ └──────────┘ └─────┘
typ ┴ ┴ └─┘ └──────────┘ └─┘ ┴ └─────┘
49 (lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m))),
id └────────────┘ └┘ └─────┘ ┴ └─┘ └──┘ └─────────┘ ┴ ┴
src └────────────┘ └──────┘ ┴ ┴ └─────┘┴ ┴ └─────┘ └──────┘ └─────────┘
typ └────────────┘ └──────┘└┘┴ ┴ └─────┘┴┴┴ └─────┘└─┘└──────┘└──┘ └─────────┘ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └─────┘ └──────┘
txt └──────┘ ┴ ┴ ┴ ┴ └─────┘ └──────┘
par └──────┘ ┴ ┴ ┴ ┴ └─────┘ └──────┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴└────┘
st └───────────────────────────────────────────────┘
50 begin
st └─────
51 cases classical.not_forall.1
id └──────────────────┘
src └────┘└──────────────────┘└──
typ └────┘└──────────────────┘└──
doc └────┘ └──
txt └────┘ └──
par └────┘ └──
pid ┴ └──
st ───────────────────────────────
52 (nat.find_min h (nat.pred_lt hl0)) with i hi,
id └──────────┘ ┴ └─────────┘ └─┘
src ───┘ └──────────┘┴ ┴ └─────────┘┴ └──────────┘
typ ───┘ └──────────┘┴┴┴ └─────────┘┴└─┘└──────────┘
doc ───┘ ┴ ┴ ┴ └──────────┘
txt ───┘ ┴ ┴ ┴ └──────────┘
par ───┘ ┴ ┴ ┴ └──────────┘
pid ───┘ ┴ ┴ ┴ └┘└────────┘
st ───────────────────────────────────────────────┘└─
53 rw [not_imp, not_lt] at hi,
id └─────┘ └────┘
src └──┘└─────┘└┘└────┘└─────┘
typ └──┘└─────┘└┘└────┘└─────┘
doc └──┘ └┘ └─────┘
txt └──┘ └┘ └─────┘
par └──┘ └┘ └─────┘
pid └┘ └┘ ┴└────┘
st ────────────┘└──────┘┴└────┘└─
54 existsi i,
id ┴
src └──────┘
typ └──────┘┴
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ──────────┘└─
55 assume j hj,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
56 have hfij : f j ≤ f i := forall_ge_le_of_forall_le_succ f hnm _ hi.1 hj,
id ┴ ┴ ┴ ┴ └────────────────────────────┘ ┴ └─┘ └┘ └┘
src └──────────┘ ┴ ┴┴┴ ┴ └──┘└────────────────────────────┘┴ ┴ └─┘ └─┘
typ └──────────┘ ┴┴┴┴┴┴┴┴└──┘└────────────────────────────┘┴┴┴└─┘└─┘└┘└─┘└┘
doc └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘
txt └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘
par └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
57 rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add'],
id └───────────┘ └────────┘ └──┘ └─────┘ └────────────────┘
src └──┘└───────────┘┴ └────────┘└─┘ └─┘└─────┘└┘└────────────────┘┴
typ └──┘└───────────┘┴ └────────┘└─┘└──┘└─┘└─────┘└┘└────────────────┘┴
doc └──┘ ┴ └─┘ └─┘ └┘ ┴
txt └──┘ ┴ └─┘ └─┘ └┘ ┴
par └──┘ ┴ └─┘ └─┘ └┘ ┴
pid └┘ ┴ └─┘ └─┘ └┘ ┴
st ──────────────────────────────────────┘└───────┘└──────────────────┘└──
58 exact calc f i ≤ a - add_monoid.smul (nat.pred l) ε : hi.2
id ┴ ┴ └─────────────┘ └──────┘ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ └──────┘┴ └┘ └─┘ └──
typ └────┘ ┴ ┴┴┴ ┴┴┴ ┴└─────────────┘┴ └──────┘┴┴└┘┴└─┘ └──
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └──
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └──
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └──
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └──
st ─────────────────────────────────────────────────────────────
59 ... = a - add_monoid.smul l ε + ε :
id ┴ ┴
src ───────┘ ┴ ┴┴┴ ┴ ┴ ┴┴┴ └──
typ ───────┘ ┴ ┴┴┴ ┴ ┴ ┴┴┴ └──
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ────────────────────────────────────────
60 by conv {to_rhs, rw [← nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero hl0), succ_smul',
id └─────────────────────┘ └────────────────┘ └─┘ └────────┘
src ─────┘ ┴└────┘└────┘└┘└────┘└─────────────────────┘┴ └────────────────┘┴ └─┘└────────┘└─
typ ─────┘ ┴└────┘└────┘└┘└────┘└─────────────────────┘┴ └────────────────┘┴└─┘└─┘└────────┘└─
doc ─────┘ ┴
txt ─────┘ ┴└────┘└────┘└┘└────┘ ┴ ┴ └─┘ └─
par ─────┘ ┴└────┘└────┘└┘└────┘ ┴ ┴ └─┘ └─
pid ─────┘ └───────────────────┘ ┴ ┴ └─┘ └─
st ───────┘└─────┘└────┘└──────────────────────────────────────────────────────┘└──────────┘└─
61 sub_add, add_sub_cancel] }
id └─────┘ └────────────┘
src ───────┘└─────┘└┘└────────────┘└┘└─
typ ───────┘└─────┘└┘└────────────┘└┘└─
txt ───────┘ └┘ └┘└─
par ───────┘ └┘ └┘└─
pid ───────┘ └┘ └───
st ──────────────┘└──────────────┘ ┴┴└
62 ... < f j + ε : add_lt_add_right (hl j (le_trans hi.1 hj)) _
id ┴ └──────────────┘ └┘ ┴ └──────┘ └┘ └┘
src ───┘└──┘ ┴ ┴ ┴ ┴ └─┘└──────────────┘┴ ┴ ┴ └──────┘┴ └─┘ └───┘
typ ───┘└──┘ ┴┴┴ ┴ ┴ └─┘└──────────────┘┴ └┘┴┴┴ └──────┘┴└┘└─┘└┘└───┘
doc └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └───┘
txt ───┘└──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └───┘
par ───┘└──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └───┘
pid ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └──┘┴
st ───┘└───────────────────────────────────────────────────────────┘
63 end
st └─┘
64
65 lemma is_cau_of_mono_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, abs (f n) ≤ a)
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
66 (hnm : ∀ n ≥ m, f n ≤ f n.succ) : is_cau_seq abs f :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ └────────┘ └─┘ ┴
src ┴ └───┘ └────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ └────────┘ └─┘ ┴
doc └────────┘
67 begin
st └─────
68 refine @eq.rec_on (ℕ → α) _ (is_cau_seq abs) _ _
id └───────┘ └────────┘
src └─────┘ └───────┘┴ ┴ ┴ └──┘ └────────┘┴ └─────
typ └─────┘ └───────┘┴ ┴ ┴ └──┘ └────────┘┴ └─────
doc └─────┘ ┴ ┴ ┴ └──┘ └────────┘┴ └─────
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ └─────
par └─────┘ ┴ ┴ ┴ └──┘ ┴ └─────
pid ┴ ┴ ┴ ┴ └──┘ ┴ └─────
st ───────────────────────────────────────────────────
69 (-⟨_, @is_cau_of_decreasing_bounded _ _ _ (λ n, -f n) a m (by simpa) (by simpa)⟩ : cau_seq α abs).2,
id ┴ └──────────────────────────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
src ───┘ ┴ └─┘ └──────────────────────────┘└─────┘ └──┘ ┴ └┘ ┴ ┴ ┴└───┘└┘ ┴└───┘└───┘└─────┘┴ ┴└─┘└─┘
typ ───┘ ┴ └─┘ └──────────────────────────┘└─────┘ └──┘ ┴┴ └┘┴┴┴┴ ┴└───┘└┘ ┴└───┘└───┘└─────┘┴┴┴└─┘└─┘
doc ───┘ └─┘ └─────┘ └──┘ ┴ └┘ ┴ ┴ ┴└───┘└┘ ┴└───┘└───┘ ┴ ┴ └─┘
txt ───┘ └─┘ └─────┘ └──┘ ┴ └┘ ┴ ┴ ┴└───┘└┘ ┴└───┘└───┘ ┴ ┴ └─┘
par ───┘ └─┘ └─────┘ └──┘ ┴ └┘ ┴ ┴ ┴└───┘└┘ ┴└───┘└───┘ ┴ ┴ └─┘
pid ───┘ └─┘ └─────┘ └──┘ ┴ └┘ ┴ ┴ └──────┘ └─────────┘ ┴ ┴ ┴└┘
st ────────────────────────────────────────────────────────────────┘└────┘└───┘└────┘└───────────────────┘└─
70 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
71 exact neg_neg _
id └─────┘
src └────┘└─────┘└─┘
typ └────┘└─────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────────┘
72 end
st └─┘
73
74 lemma is_cau_series_of_abv_le_cau {f : ℕ → β} {g : ℕ → α} (n : ℕ) : (∀ m, n ≤ m → abv (f m) ≤ g m) →
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
75 is_cau_seq abs (λ n, (range n).sum g) → is_cau_seq abv (λ n, (range n).sum f) :=
id └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
src └────────┘ └─┘ ┴ └───┘ └─┘ └────────┘ └───┘ └─┘
typ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
doc └────────┘ └───┘ └────────┘ └───┘
76 begin
st └─────
77 assume hm hg ε ε0,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └───────────────┘
st ──────────────────┘└─
78 cases hg (ε / 2) (div_pos ε0 (by norm_num)) with i hi,
id └┘ ┴ ┴ └─────┘ └┘
src └────┘ ┴ ┴┴└──┘ └─────┘┴ ┴ ┴└──────┘└──────────┘
typ └────┘└┘┴ ┴┴┴└──┘ └─────┘┴└┘┴ ┴└──────┘└──────────┘
doc └────┘ ┴ ┴ └──┘ ┴ ┴ ┴└──────┘└──────────┘
txt └────┘ ┴ ┴ └──┘ ┴ ┴ ┴└──────┘└──────────┘
par └────┘ ┴ ┴ └──┘ ┴ ┴ ┴└──────┘└──────────┘
pid ┴ ┴ ┴ └──┘ ┴ ┴ └─────────┘└────────┘
st ─────────────────────────────────┘└───────┘└──────────┘└─
79 existsi max n i,
id └─┘ ┴ ┴
src └──────┘└─┘┴ ┴
typ └──────┘└─┘┴┴┴┴
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘└─
80 assume j ji,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
81 have hi₁ := hi j (le_trans (le_max_right n i) ji),
id └┘ ┴ └──────┘ └──────────┘ ┴ ┴ └┘
src └──────────┘ ┴ ┴ └──────┘┴ └──────────┘┴ ┴ └┘ ┴
typ └──────────┘└┘┴┴┴ └──────┘┴ └──────────┘┴┴┴┴└┘└┘┴
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par └──────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid └──────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────┘└─
82 have hi₂ := hi (max n i) (le_max_right n i),
id └┘ └─┘ └──────────┘ ┴ ┴
src └──────────┘ ┴ └─┘┴ ┴ └┘ └──────────┘┴ ┴ ┴
typ └──────────┘└┘┴ └─┘┴ ┴ └┘ └──────────┘┴┴┴┴┴
doc └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └──────┘┴└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────┘└─
83 have sub_le := abs_sub_le ((range j).sum g) ((range i).sum g) ((range (max n i)).sum g),
id └────────┘ ┴ └───┘ └─┘ ┴ ┴ ┴
src └─────────────┘└────────┘┴ ┴ └────┘ └┘ ┴ └────┘ └┘ └───┘┴ └─┘┴ ┴ └─────┘ ┴
typ └─────────────┘└────────┘┴ ┴┴└────┘ └┘ ┴ └────┘ └┘ └───┘┴ └─┘┴┴┴┴└─────┘┴┴
doc └─────────────┘ ┴ ┴ └────┘ └┘ ┴ └────┘ └┘ └───┘┴ ┴ ┴ └─────┘ ┴
txt └─────────────┘ ┴ ┴ └────┘ └┘ ┴ └────┘ └┘ ┴ ┴ ┴ └─────┘ ┴
par └─────────────┘ ┴ ┴ └────┘ └┘ ┴ └────┘ └┘ ┴ ┴ ┴ └─────┘ ┴
pid └─────────┘┴└─┘ ┴ ┴ └────┘ └┘ ┴ └────┘ └┘ ┴ ┴ ┴ └─────┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
84 have := add_lt_add hi₁ hi₂,
id └────────┘ └─┘ └─┘
src └──────┘└────────┘┴ ┴
typ └──────┘└────────┘┴└─┘┴└─┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ───────────────────────────┘└─
85 rw [abs_sub ((range (max n i)).sum g), add_halves ε] at this,
id └─────┘ └───┘ └─┘ ┴ ┴ ┴ └────────┘ ┴
src └──┘└─────┘┴ └───┘┴ └─┘┴ ┴ └─────┘ └─┘└────────┘┴ └───────┘
typ └──┘└─────┘┴ └───┘┴ └─┘┴┴┴┴└─────┘┴└─┘└────────┘┴┴└───────┘
doc └──┘ ┴ └───┘┴ ┴ ┴ └─────┘ └─┘ ┴ └───────┘
txt └──┘ ┴ ┴ ┴ ┴ └─────┘ └─┘ ┴ └───────┘
par └──┘ ┴ ┴ ┴ ┴ └─────┘ └─┘ ┴ └───────┘
pid └┘ ┴ ┴ ┴ ┴ └─────┘ └─┘ ┴ ┴└──────┘
st ──────────────────────────────────────┘└────────────┘┴└──────┘└─
86 refine lt_of_le_of_lt (le_trans (le_trans _ (le_abs_self _)) sub_le) this,
id └────────────┘ └──────┘ └─────────┘ └────┘ └──┘
src └─────┘└────────────┘┴ ┴ └──────┘└─┘ └─────────┘└───┘└────┘└┘
typ └─────┘└────────────┘┴ ┴ └──────┘└─┘ └─────────┘└───┘└────┘└┘└──┘
doc └─────┘ ┴ ┴ └─┘ └───┘ └┘
txt └─────┘ ┴ ┴ └─┘ └───┘ └┘
par └─────┘ ┴ ┴ └─┘ └───┘ └┘
pid ┴ ┴ ┴ └─┘ └───┘ └┘
st ──────────────────────────────────────────────────────────────────────────┘└─
87 generalize hk : j - max n i = k,
id ┴ ┴ └─┘ ┴ ┴
src └──────────────┘ ┴┴┴└─┘┴ ┴ ┴ ┴
typ └──────────────┘┴┴┴┴└─┘┴┴┴┴┴ ┴
doc └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─┘└┘┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────┘└─
88 clear this hi₂ hi₁ hi ε0 ε hg sub_le,
src └──────────────────────────────────┘
typ └──────────────────────────────────┘
doc └──────────────────────────────────┘
txt └──────────────────────────────────┘
par └──────────────────────────────────┘
pid └─────────────────────────────┘
st ─────────────────────────────────────┘└─
89 rw nat.sub_eq_iff_eq_add ji at hk,
id └───────────────────┘ └┘
src └─┘└───────────────────┘┴ └────┘
typ └─┘└───────────────────┘┴└┘└────┘
doc └─┘ ┴ └────┘
txt └─┘ ┴ └────┘
par └─┘ ┴ └────┘
pid ┴ ┴ └────┘
st ──────────────────────────────────┘└─
90 rw hk,
id └┘
src └─┘
typ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────┘└─
91 clear hk ji j,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └──────┘
st ──────────────┘└─
92 induction k with k' hi,
id ┴
src └────────┘ └─────────┘
typ └────────┘┴└─────────┘
doc └────────┘ └─────────┘
txt └────────┘ └─────────┘
par └────────┘ └─────────┘
pid ┴ ┴└────────┘
st ───────────────────────┘└─
93 { simp [abv_zero abv] },
id └──────┘ └─┘
src └────┘└──────┘┴ └┘
typ └────┘└──────┘┴└─┘└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴┴ ┴ ┴┴
st ───┘└──────────────────┘└┘└
94 { dsimp at *,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└──┘
st ─────────────┘└─
95 rw [nat.succ_add, sum_range_succ, sum_range_succ, add_assoc, add_assoc],
id └──────────┘ └────────────┘ └────────────┘ └───────┘ └───────┘
src └──┘└──────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘└┘└───────┘┴
typ └──┘└──────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘└┘└───────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────┘└──────────────┘└──────────────┘└─────────┘└─────────┘└──
96 refine le_trans (abv_add _ _ _) _,
id └──────┘ └─────┘
src └─────┘└──────┘┴ └─────┘└───────┘
typ └─────┘└──────┘┴ └─────┘└───────┘
doc └─────┘ ┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ────────────────────────────────────┘└─
97 exact add_le_add (hm _ (le_add_of_nonneg_of_le (nat.zero_le _) (le_max_left _ _))) hi },
id └────────┘ └┘ └────────────────────┘ └─────────┘ └─────────┘ └┘
src └────┘└────────┘┴ └─┘ └────────────────────┘┴ └─────────┘└──┘ └─────────┘└──────┘ ┴
typ └────┘└────────┘┴ └┘└─┘ └────────────────────┘┴ └─────────┘└──┘ └─────────┘└──────┘└┘┴
doc └────┘ ┴ └─┘ ┴ └──┘ └──────┘ ┴
txt └────┘ ┴ └─┘ ┴ └──┘ └──────┘ ┴
par └────┘ ┴ └─┘ ┴ └──┘ └──────┘ ┴
pid ┴ ┴ └─┘ ┴ └──┘ └──────┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└──
98 end
st ──┘
99
100 lemma is_cau_series_of_abv_cau {f : ℕ → β} : is_cau_seq abs (λ m, (range m).sum (λ n, abv (f n))) →
id ┴ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └─┘ ┴ ┴
src ┴ └────────┘ └─┘ └───┘ └─┘
typ ┴ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └─┘ ┴ ┴
doc └────────┘ └───┘
101 is_cau_seq abv (λ m, (range m).sum f) :=
id └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
src └────────┘ └───┘ └─┘
typ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
doc └────────┘ └───┘
102 is_cau_series_of_abv_le_cau 0 (λ n h, le_refl _)
id └─────────────────────────┘ ┴ ┴ └─────┘
src └─────────────────────────┘ └─────┘
typ └─────────────────────────┘ ┴ ┴ └─────┘
103
104 lemma is_cau_geo_series {β : Type*} [field β] {abv : β → α} [is_absolute_value abv]
id └───┘ ┴ ┴ ┴ └───────────────┘ └─┘
src └───┘ └───────────────┘
typ └───┘ ┴ ┴ ┴ └───────────────┘ └─┘
doc └───────────────┘
105 (x : β) (hx1 : abv x < 1) : is_cau_seq abv (λ n, (range n).sum (λ m, x ^ m)) :=
id ┴ └─┘ ┴ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └────────┘ └───┘ └─┘ ┴
typ ┴ └─┘ ┴ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └────────┘ └───┘
st ┴
106 have hx1' : abv x ≠ 1 := λ h, by simpa [h, lt_irrefl] using hx1,
id └─┘ ┴ ┴ ┴ ┴ └───────┘ └─┘
src ┴ └─────┘ └┘└───────┘└──────┘
typ └─┘ ┴ ┴ ┴ └─────┘┴└┘└───────┘└──────┘└─┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └─────────────────────────────┘
107 is_cau_series_of_abv_cau
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
108 begin
st └─────
109 simp only [abv_pow abv] {eta := ff},
id └─────┘ └─┘ └┘
src └─────────┘└─────┘┴ └┘ └─────┘└┘┴
typ └─────────┘└─────┘┴└─┘└┘ └─────┘└┘┴
doc └─────────┘ ┴ └┘ └─────┘ ┴
txt └─────────┘ ┴ └┘ └─────┘ ┴
par └─────────┘ ┴ └┘ └─────┘ ┴
pid ┴└──┘└┘ ┴ ┴┴ └─────┘ ┴
st ────────────────────────────────────┘└─
110 have : (λ (m : ℕ), (range m).sum (λ n, (abv x) ^ n)) =
id └───┘ ┴ ┴
src └─────┘ └────┘ └─┘ └───┘┴ └────┘ └──┘ ┴ └┘┴┴ └─┘┴└
typ └─────┘ └────┘ └─┘ └───┘┴ └────┘ └──┘ ┴ └┘┴┴ └─┘┴└
doc └─────┘ └────┘ └─┘ └───┘┴ └────┘ └──┘ ┴ └┘ ┴ └─┘ └
txt └─────┘ └────┘ └─┘ ┴ └────┘ └──┘ ┴ └┘ ┴ └─┘ └
par └─────┘ └────┘ └─┘ ┴ └────┘ └──┘ ┴ └┘ ┴ └─┘ └
pid └───┘└┘ └────┘ └─┘ ┴ └────┘ └──┘ ┴ └┘ ┴ └─┘ └
st ─────────────────────────────────────────────────────────
111 λ m, geom_series (abv x) m := rfl,
id └─────────┘ └─┘ ┴ └─┘
src ──┘ └──┘└─────────┘┴ ┴ └┘ └──┘└─┘
typ ──┘ └──┘└─────────┘┴ └─┘┴┴└┘ └──┘└─┘
doc ──┘ └──┘└─────────┘┴ ┴ └┘ └──┘
txt ──┘ └──┘ ┴ ┴ └┘ └──┘
par ──┘ └──┘ ┴ ┴ └┘ └──┘
pid ──┘ └──┘ ┴ ┴ └┘ └──┘
st ───────────────────────────────────┘└─
112 simp only [this, geom_sum hx1'] {eta := ff},
id └──┘ └──────┘ └──┘ └┘
src └─────────┘ └┘└──────┘┴ └┘ └─────┘└┘┴
typ └─────────┘└──┘└┘└──────┘┴└──┘└┘ └─────┘└┘┴
doc └─────────┘ └┘ ┴ └┘ └─────┘ ┴
txt └─────────┘ └┘ ┴ └┘ └─────┘ ┴
par └─────────┘ └┘ ┴ └┘ └─────┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴┴ └─────┘ ┴
st ────────────────────────────────────────────┘└─
113 conv in (_ / _) { rw [← neg_div_neg_eq, neg_sub, neg_sub] },
id ┴ └────────────┘ └─────┘ └─────┘
src └──────┘ └┘┴└────┘└────┘└────────────┘└┘└─────┘└┘└─────┘└┘┴
typ └──────┘ └┘┴└────┘└────┘└────────────┘└┘└─────┘└┘└─────┘└┘┴
txt └──────┘ └┘ └────┘└────┘ └┘ └┘ └┘┴
par └──────┘ └┘ └────┘└────┘ └┘ └┘ └┘┴
pid ┴└─┘ └┘ └─┘└───────┘ └┘ └┘ └─┘
st ──────────────────┘└───────────────────┘└───────┘└───────┘ ┴└┘└
114 refine @is_cau_of_mono_bounded _ _ _ _ ((1 : α) / (1 - abv x)) 0 _ _,
id └────────────────────┘ ┴ ┴ └─┘ ┴
src └─────┘ └────────────────────┘└───────┘ └──┘ └┘ ┴ └┘┴┴ ┴ └──────┘
typ └─────┘ └────────────────────┘└───────┘ └──┘┴└┘ ┴ └┘┴┴└─┘┴┴└──────┘
doc └─────┘ └───────┘ └──┘ └┘ ┴ └┘ ┴ ┴ └──────┘
txt └─────┘ └───────┘ └──┘ └┘ ┴ └┘ ┴ ┴ └──────┘
par └─────┘ └───────┘ └──┘ └┘ ┴ └┘ ┴ ┴ └──────┘
pid ┴ └───────┘ └──┘ └┘ ┴ └┘ ┴ ┴ └──────┘
st ─────────────────────────────────────────────────────────────────────┘└─
115 { assume n hn,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
116 rw abs_of_nonneg,
id └───────────┘
src └─┘└───────────┘
typ └─┘└───────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────┘└─
117 refine div_le_div_of_le_of_pos (sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _))
id └─────────────────────┘ └─────────┘ └─────┘ └─┘ ┴ ┴ ┴ └────────┘
src └─────┘└─────────────────────┘┴ └─────────┘└─┘ └─────┘┴ ┴ ┴ ┴┴┴└────────┘└──────
typ └─────┘└─────────────────────┘┴ └─────────┘└─┘ └─────┘┴└─┘┴┴┴┴┴┴┴└────────┘└──────
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
par └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
pid ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
st ──────────────────────────────────────────────────────────────────────────────────────
118 (sub_pos.2 hx1),
id └─────┘ └─┘
src ─────┘ └─────┘└─┘ ┴
typ ─────┘ └─────┘└─┘└─┘┴
doc ─────┘ └─┘ ┴
txt ─────┘ └─┘ ┴
par ─────┘ └─┘ ┴
pid ─────┘ └─┘ ┴
st ────────────────────┘└─
119 refine div_nonneg (sub_nonneg.2 _) (sub_pos.2 hx1),
id └────────┘ └────────┘ └─────┘ └─┘
src └─────┘└────────┘┴ └────────┘└────┘ └─────┘└─┘ ┴
typ └─────┘└────────┘┴ └────────┘└────┘ └─────┘└─┘└─┘┴
doc └─────┘ ┴ └────┘ └─┘ ┴
txt └─────┘ ┴ └────┘ └─┘ ┴
par └─────┘ ┴ └────┘ └─┘ ┴
pid ┴ ┴ └────┘ └─┘ ┴
st ─────────────────────────────────────────────────────┘└─
120 clear hn,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ───────────┘└─
121 induction n with n ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ────────────────────────┘└─
122 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────┘└───┘└┘└
123 { rw [_root_.pow_succ, ← one_mul (1 : α)],
id └─────────────┘ └─────┘ ┴
src └──┘└─────────────┘└──┘└─────┘┴ └──┘ └┘
typ └──┘└─────────────┘└──┘└─────┘┴ └──┘┴└┘
doc └──┘ └──┘ ┴ └──┘ └┘
txt └──┘ └──┘ ┴ └──┘ └┘
par └──┘ └──┘ ┴ └──┘ └┘
pid └┘ └──┘ ┴ └──┘ └┘
st ────────────────────────┘└─────────────────┘┴└─
124 refine mul_le_mul (le_of_lt hx1) ih (abv_pow abv x n ▸ abv_nonneg _ _) (by norm_num) } },
id └────────┘ └──────┘ └─┘ └┘ └─────┘ └─┘ ┴ ┴ └────────┘
src └─────┘└────────┘┴ └──────┘┴ └┘ ┴ └─────┘┴ ┴ ┴ ┴ ┴└────────┘└────┘ ┴└──────┘└┘
typ └─────┘└────────┘┴ └──────┘┴└─┘└┘└┘┴ └─────┘┴└─┘┴┴┴┴┴ ┴└────────┘└────┘ ┴└──────┘└┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴└──────┘└┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴└──────┘└┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴└──────┘└┘
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └────────┘┴
st ───────────────────────────────────────────────────────────────────────────────┘└───────┘└┘└──┘└
125 { assume n hn,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
126 refine div_le_div_of_le_of_pos (sub_le_sub_left _ _) (sub_pos.2 hx1),
id └─────────────────────┘ └─────────────┘ └─────┘ └─┘
src └─────┘└─────────────────────┘┴ └─────────────┘└────┘ └─────┘└─┘ ┴
typ └─────┘└─────────────────────┘┴ └─────────────┘└────┘ └─────┘└─┘└─┘┴
doc └─────┘ ┴ └────┘ └─┘ ┴
txt └─────┘ ┴ └────┘ └─┘ ┴
par └─────┘ ┴ └────┘ └─┘ ┴
pid ┴ ┴ └────┘ └─┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
127 rw [← one_mul (_ ^ n), _root_.pow_succ],
id └─────┘ ┴ └─────────────┘
src └────┘└─────┘┴ └┘ ┴ └─┘└─────────────┘┴
typ └────┘└─────┘┴ └┘ ┴┴└─┘└─────────────┘┴
doc └────┘ ┴ └┘ ┴ └─┘ ┴
txt └────┘ ┴ └┘ ┴ └─┘ ┴
par └────┘ ┴ └┘ ┴ └─┘ ┴
pid └──┘ ┴ └┘ ┴ └─┘ ┴
st ────────────────────────┘└───────────────┘└──
128 exact mul_le_mul_of_nonneg_right (le_of_lt hx1) (pow_nonneg (abv_nonneg _ _) _) }
id └────────────────────────┘ └──────┘ └─┘ └────────┘ └────────┘
src └────┘└────────────────────────┘┴ └──────┘┴ └┘ └────────┘┴ └────────┘└───────┘
typ └────┘└────────────────────────┘┴ └──────┘┴└─┘└┘ └────────┘┴ └────────┘└───────┘
doc └────┘ ┴ ┴ └┘ ┴ └───────┘
txt └────┘ ┴ ┴ └┘ ┴ └───────┘
par └────┘ ┴ ┴ └┘ ┴ └───────┘
pid ┴ ┴ ┴ └┘ ┴ └──────┘┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
129 end
st ──┘
130
131 lemma is_cau_geo_series_const (a : α) {x : α} (hx1 : abs x < 1) : is_cau_seq abs (λ m, (range m).sum (λ n, a * x ^ n)) :=
id ┴ ┴ └─┘ ┴ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └────────┘ └─┘ └───┘ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └───┘
132 have is_cau_seq abs (λ m, a * (range m).sum (λ n, x ^ n)) := (cau_seq.const abs a * ⟨_, is_cau_geo_series x hx1⟩).2,
id └────────┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───────────┘ └─┘ ┴ ┴ └───────────────┘ ┴ └─┘ ┴
src └────────┘ └─┘ ┴ └───┘ └─┘ ┴ └───────────┘ └─┘ ┴ └───────────────┘ ┴
typ └────────┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───────────┘ └─┘ ┴ ┴ └───────────────┘ ┴ └─┘ ┴
doc └────────┘ └───┘ └───────────┘
133 by simpa only [mul_sum]
id └─────┘
src └──────────┘└─────┘└─
typ └──────────┘└─────┘└─
doc └──────────┘ └─
txt └──────────┘ └─
par └──────────┘ └─
pid ┴└──┘└┘ ┴└
st └─────────────────────
134
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
135 lemma series_ratio_test {f : ℕ → β} (n : ℕ) (r : α)
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
136 (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ m, n ≤ m → abv (f m.succ) ≤ r * abv (f m)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└───┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └───┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└───┘ ┴ ┴ ┴ └─┘ ┴ ┴
137 is_cau_seq abv (λ m, (range m).sum f) :=
id └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
src └────────┘ └───┘ └─┘
typ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
doc └────────┘ └───┘
138 have har1 : abs r < 1, by rwa abs_of_nonneg hr0,
id └─┘ ┴ ┴ └───────────┘ └─┘
src └─┘ ┴ └──┘└───────────┘┴
typ └─┘ ┴ ┴ └──┘└───────────┘┴└─┘
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st └────────────────────┘
139 begin
st └─────
140 refine is_cau_series_of_abv_le_cau n.succ _ (is_cau_geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1),
id └─────────────────────────┘ └─────────────────────┘ └─┘ ┴ ┴ ┴└┘ ┴ └────┘ └──┘
src └─────┘└─────────────────────────┘┴ └─┘ └─────────────────────┘┴ ┴ ┴ └┘┴┴ └┘┴┴┴└────┘└┘ ┴
typ └─────┘└─────────────────────────┘┴ └─┘ └─────────────────────┘┴ └─┘┴ ┴┴ └┘┴┴┴└┘┴┴┴└────┘└┘└──┘┴
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
pid ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
141 assume m hmn,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ─────────────┘└─
142 cases classical.em (r = 0) with r_zero r_ne_zero,
id └──────────┘ ┴ ┴
src └────┘└──────────┘┴ ┴┴└───────────────────────┘
typ └────┘└──────────┘┴ ┴┴┴└───────────────────────┘
doc └────┘ ┴ ┴ └───────────────────────┘
txt └────┘ ┴ ┴ └───────────────────────┘
par └────┘ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ └─┘└────────────────────┘
st ─────────────────────────────────────────────────┘└─
143 { have m_pos := lt_of_lt_of_le (nat.succ_pos n) hmn,
id └────────────┘ └──────────┘ ┴ └─┘
src └────────────┘└────────────┘┴ └──────────┘┴ └┘
typ └────────────┘└────────────┘┴ └──────────┘┴┴└┘└─┘
doc └────────────┘ ┴ ┴ └┘
txt └────────────┘ ┴ ┴ └┘
par └────────────┘ ┴ ┴ └┘
pid └────────┘┴└─┘ ┴ ┴ └┘
st ───┘└───────────────────────────────────────────────┘└─
144 have := h m.pred (nat.le_of_succ_le_succ (by rwa [nat.succ_pred_eq_of_pos m_pos])),
id ┴ └────┘ └────────────────────┘ └─────────────────────┘ └───┘
src └──────┘ ┴└────┘┴ └────────────────────┘┴ ┴└───┘└─────────────────────┘┴ ┴└┘
typ └──────┘┴┴└────┘┴ └────────────────────┘┴ ┴└───┘└─────────────────────┘┴└───┘┴└┘
doc └──────┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴└┘
txt └──────┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴└┘
par └──────┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴└┘
pid └───┘└─┘ ┴ ┴ ┴ └────┘ ┴ └─┘
st ───────────────────────────────────────────────┘└─────────────────────────────────┘┴└┘└─
145 simpa [r_zero, nat.succ_pred_eq_of_pos m_pos, pow_succ] },
id └────┘ └─────────────────────┘ └───┘ └──────┘
src └─────┘ └┘└─────────────────────┘┴ └┘└──────┘└┘
typ └─────┘└────┘└┘└─────────────────────┘┴└───┘└┘└──────┘└┘
doc └─────┘ └┘ ┴ └┘ └┘
txt └─────┘ └┘ ┴ └┘ └┘
par └─────┘ └┘ ┴ └┘ └┘
pid ┴┴ └┘ ┴ └┘ ┴┴
st ───────────────────────────────────────────────────────────┘└┘└
146 generalize hk : m - n.succ = k,
id ┴ ┴ └────┘
src └──────────────┘ ┴┴┴└────┘┴ ┴
typ └──────────────┘┴┴┴┴└────┘┴ ┴
doc └──────────────┘ ┴ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ ┴ ┴
pid └─┘└┘┴ ┴ ┴ ┴ ┴
st ───────────────────────────────┘└─
147 have r_pos : 0 < r := lt_of_le_of_ne hr0 (ne.symm r_ne_zero),
id ┴ ┴ └────────────┘ └─┘ └─────┘ └───────┘
src └─────────────┘┴┴ └──┘└────────────┘┴ ┴ └─────┘┴ ┴
typ └─────────────┘┴┴┴└──┘└────────────┘┴└─┘┴ └─────┘┴└───────┘┴
doc └─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
txt └─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
par └─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
pid └────────┘└───┘ ┴ └──┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
148 replace hk : m = k + n.succ := (nat.sub_eq_iff_eq_add hmn).1 hk,
id ┴ ┴ ┴ └────┘ └───────────────────┘ └─┘ └┘
src └───────────┘ ┴ ┴ ┴┴┴└────┘└──┘ └───────────────────┘┴ └──┘
typ └───────────┘┴┴ ┴┴┴┴┴└────┘└──┘ └───────────────────┘┴└─┘└──┘└┘
doc └───────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
txt └───────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
par └───────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
pid └─┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘
st ────────────────────────────────────────────────────────────────┘└─
149 induction k with k ih generalizing m n,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
150 { rw [hk, zero_add, mul_right_comm, ← pow_inv _ _ r_ne_zero, ← div_eq_mul_inv, mul_div_cancel],
id └┘ └──────┘ └────────────┘ └─────┘ └───────┘ └────────────┘ └────────────┘
src └──┘ └┘└──────┘└┘└────────────┘└──┘└─────┘└───┘ └──┘└────────────┘└┘└────────────┘┴
typ └──┘└┘└┘└──────┘└┘└────────────┘└──┘└─────┘└───┘└───────┘└──┘└────────────┘└┘└────────────┘┴
doc └──┘ └┘ └┘ └──┘ └───┘ └──┘ └┘ ┴
txt └──┘ └┘ └┘ └──┘ └───┘ └──┘ └┘ ┴
par └──┘ └┘ └┘ └──┘ └───┘ └──┘ └┘ ┴
pid └┘ └┘ └┘ └──┘ └───┘ └──┘ └┘ ┴
st ───┘└────┘└────────┘└──────────────┘└───────────────────────┘└────────────────┘└──────────────┘┴└─
151 exact (ne_of_lt (pow_pos r_pos _)).symm },
id └──────┘ └─────┘ └───┘
src └────┘ └──────┘┴ └─────┘┴ └────────┘
typ └────┘ └──────┘┴ └─────┘┴└───┘└────────┘
doc └────┘ ┴ ┴ └────────┘
txt └────┘ ┴ ┴ └────────┘
par └────┘ ┴ ┴ └────────┘
pid ┴ ┴ ┴ └──────┘└┘
st ───────────────────────────────────────────┘└┘└
152 { have kn : k + n.succ ≥ n.succ, by rw ← zero_add n.succ; exact add_le_add (zero_le _) (by simp),
id ┴ ┴ └────┘ └──────┘ └────┘ └────────┘ └─────┘
src └────────┘ ┴ ┴ ┴┴┴└────┘ └───┘└──────┘┴└────┘ └────┘└────────┘┴ └─────┘└──┘ ┴└──┘┴
typ └────────┘┴┴ ┴ ┴┴┴└────┘ └───┘└──────┘┴└────┘ └────┘└────────┘┴ └─────┘└──┘ ┴└──┘┴
doc └────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ └──┘ ┴└──┘┴
txt └────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ └──┘ ┴└──┘┴
par └────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ └──┘ ┴└──┘┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └────┘
st ────────────────────────────────┘ └───┘ └─
153 rw [hk, nat.succ_add, pow_succ' r, ← mul_assoc],
id └┘ └──────────┘ └───────┘ ┴ └───────┘
src └──┘ └┘└──────────┘└┘└───────┘┴ └──┘└───────┘┴
typ └──┘└┘└┘└──────────┘└┘└───────┘┴┴└──┘└───────┘┴
doc └──┘ └┘ └┘ ┴ └──┘ ┴
txt └──┘ └┘ └┘ ┴ └──┘ ┴
par └──┘ └┘ └┘ ┴ └──┘ ┴
pid └┘ └┘ └┘ ┴ └──┘ ┴
st ─────────┘└────────────┘└───────────┘└───────────┘└──
154 exact le_trans (by rw mul_comm; exact h _ (nat.le_of_succ_le kn))
id └──────┘ └──────┘ ┴ └───────────────┘ └┘
src └────┘└──────┘┴ ┴└─┘└──────┘└──────┘ └─┘ └───────────────┘┴ └──
typ └────┘└──────┘┴ ┴└─┘└──────┘└──────┘┴└─┘ └───────────────┘┴└┘└──
doc └────┘ ┴ ┴└─┘ └──────┘ └─┘ ┴ └──
txt └────┘ ┴ ┴└─┘ └──────┘ └─┘ ┴ └──
par └────┘ ┴ ┴└─┘ └──────┘ └─┘ ┴ └──
pid ┴ ┴ └──┘ └──────┘ └─┘ ┴ └──
st ─────────────────────┘└────────────────────────────────────────────┘└─
155 (mul_le_mul_of_nonneg_right (ih (k + n.succ) n h kn rfl) hr0) }
id └────────────────────────┘ └┘ ┴ └────┘ ┴ ┴ └┘ └─┘ └─┘
src ─────┘ └────────────────────────┘┴ ┴ ┴ ┴└────┘└┘ ┴ ┴ ┴└─┘└┘ └┘
typ ─────┘ └────────────────────────┘┴ └┘┴ ┴┴ ┴└────┘└┘┴┴┴┴└┘┴└─┘└┘└─┘└┘
doc ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
txt ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
par ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
pid ─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────┘└─
156 end
st ──┘
157
158 lemma sum_range_diag_flip {α : Type*} [add_comm_monoid α] (n : ℕ) (f : ℕ → ℕ → α) :
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴
159 (range n).sum (λ m, (range (m + 1)).sum (λ k, f k (m - k))) =
id └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └─┘ └───┘ ┴ └─┘ ┴ ┴
typ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
160 (range n).sum (λ m, (range (n - m)).sum (f m)) :=
id └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └───┘ └─┘ └───┘ ┴ └─┘
typ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └───┘ └───┘
161 have h₁ : ((range n).sigma (range ∘ nat.succ)).sum
id └───┘ ┴ └───┘ └───┘ ┴ └──────┘ └─┘
src └───┘ └───┘ └───┘ ┴ └──────┘ └─┘
typ └───┘ ┴ └───┘ └───┘ ┴ └──────┘ └─┘
doc └───┘ └───┘ └───┘
162 (λ (a : Σ m, ℕ), f (a.2) (a.1 - a.2)) =
id ┴ ┴┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴
163 (range n).sum (λ m, (range (m + 1)).sum
id └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └─┘
src └───┘ └─┘ └───┘ ┴ └─┘
typ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └─┘
doc └───┘ └───┘
164 (λ k, f k (m - k))) := sum_sigma,
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
165 have h₂ : ((range n).sigma (λ m, range (n - m))).sum (λ a : Σ (m : ℕ), ℕ, f (a.1) (a.2)) =
id └───┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
src └───┘ └───┘ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
doc └───┘ └───┘ └───┘
166 (range n).sum (λ m, sum (range (n - m)) (f m)) := sum_sigma,
id └───┘ ┴ └─┘ ┴ └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───────┘
src └───┘ └─┘ └─┘ └───┘ ┴ └───────┘
typ └───┘ ┴ └─┘ ┴ └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───────┘
doc └───┘ └───┘
167 h₁ ▸ h₂ ▸ sum_bij
id └┘ ┴ └┘ ┴ └─────┘
src ┴ ┴ └─────┘
typ └┘ ┴ └┘ ┴ └─────┘
168 (λ a _, ⟨a.2, a.1 - a.2⟩)
id ┴ ┴ ┴┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴
169 (λ a ha, have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1,
id ┴ └┘ ┴┴ ┴ ┴ └───────┘┴ └───────┘┴ └┘ ┴
src ┴ ┴ └───────┘┴ └───────┘┴ ┴
typ ┴ └┘ ┴┴ ┴ ┴ └───────┘┴ └───────┘┴ └┘ ┴
170 have h₂ : a.2 < nat.succ a.1 := mem_range.1 (mem_sigma.1 ha).2,
id ┴┴ ┴ └──────┘ ┴┴ └───────┘┴ └───────┘┴ └┘ ┴
src ┴ ┴ └──────┘ ┴ └───────┘┴ └───────┘┴ ┴
typ ┴┴ ┴ └──────┘ ┴┴ └───────┘┴ └───────┘┴ └┘ ┴
171 mem_sigma.2 ⟨mem_range.2 (lt_of_lt_of_le h₂ h₁),
id └───────┘┴ └───────┘┴ └────────────┘ └┘ └┘
src └───────┘┴ └───────┘┴ └────────────┘
typ └───────┘┴ └───────┘┴ └────────────┘ └┘ └┘
172 mem_range.2 ((nat.sub_lt_sub_right_iff (nat.le_of_lt_succ h₂)).2 h₁)⟩)
id └───────┘┴ └──────────────────────┘ └───────────────┘ └┘ ┴ └┘
src └───────┘┴ └──────────────────────┘ └───────────────┘ ┴
typ └───────┘┴ └──────────────────────┘ └───────────────┘ └┘ ┴ └┘
173 (λ _ _, rfl)
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
174 (λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h,
id ┴└┘ └┘ ┴└┘ └┘ └┘ └┘ ┴
typ ┴└┘ └┘ ┴└┘ └┘ └┘ └┘ ┴
175 have ha : a₁ < n ∧ a₂ ≤ a₁ :=
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
176 ⟨mem_range.1 (mem_sigma.1 ha).1, nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 ha).2)⟩,
id └───────┘┴ └───────┘┴ └┘ ┴ └───────────────┘ └───────┘┴ └───────┘┴ └┘ ┴
src └───────┘┴ └───────┘┴ ┴ └───────────────┘ └───────┘┴ └───────┘┴ ┴
typ └───────┘┴ └───────┘┴ └┘ ┴ └───────────────┘ └───────┘┴ └───────┘┴ └┘ ┴
177 have hb : b₁ < n ∧ b₂ ≤ b₁ :=
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
178 ⟨mem_range.1 (mem_sigma.1 hb).1, nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 hb).2)⟩,
id └───────┘┴ └───────┘┴ └┘ ┴ └───────────────┘ └───────┘┴ └───────┘┴ └┘ ┴
src └───────┘┴ └───────┘┴ ┴ └───────────────┘ └───────┘┴ └───────┘┴ ┴
typ └───────┘┴ └───────┘┴ └┘ ┴ └───────────────┘ └───────┘┴ └───────┘┴ └┘ ┴
179 have h : a₂ = b₂ ∧ _ := sigma.mk.inj h,
id ┴ ┴ └──────────┘ ┴
src ┴ ┴ └──────────┘
typ ┴ ┴ └──────────┘ ┴
180 have h' : a₁ = b₁ - b₂ + a₂ := (nat.sub_eq_iff_eq_add ha.2).1 (eq_of_heq h.2),
id ┴ ┴ ┴ └───────────────────┘ └┘┴ ┴ └───────┘ ┴┴
src ┴ ┴ ┴ └───────────────────┘ ┴ ┴ └───────┘ ┴
typ ┴ ┴ ┴ └───────────────────┘ └┘┴ ┴ └───────┘ ┴┴
181 sigma.mk.inj_iff.2
id └──────────────┘┴
src └──────────────┘┴
typ └──────────────┘┴
182 ⟨nat.sub_add_cancel hb.2 ▸ h'.symm ▸ h.1 ▸ rfl,
id └────────────────┘ └┘┴ ┴ └┘└───┘ ┴ ┴┴ ┴ └─┘
src └────────────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘
typ └────────────────┘ └┘┴ ┴ └┘└───┘ ┴ ┴┴ ┴ └─┘
183 (heq_of_eq h.1)⟩)
id └───────┘ ┴┴
src └───────┘ ┴
typ └───────┘ ┴┴
184 (λ ⟨a₁, a₂⟩ ha,
id ┴└┘ └┘ └┘
typ ┴└┘ └┘ └┘
185 have ha : a₁ < n ∧ a₂ < n - a₁ :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
186 ⟨mem_range.1 (mem_sigma.1 ha).1, (mem_range.1 (mem_sigma.1 ha).2)⟩,
id └───────┘┴ └───────┘┴ └┘ ┴ └───────┘┴ └───────┘┴ └┘ ┴
src └───────┘┴ └───────┘┴ ┴ └───────┘┴ └───────┘┴ ┴
typ └───────┘┴ └───────┘┴ └┘ ┴ └───────┘┴ └───────┘┴ └┘ ┴
187 ⟨⟨a₂ + a₁, a₁⟩, ⟨mem_sigma.2 ⟨mem_range.2 (nat.lt_sub_right_iff_add_lt.1 ha.2),
id ┴ └───────┘┴ └───────┘┴ └─────────────────────────┘┴ └┘┴
src ┴ └───────┘┴ └───────┘┴ └─────────────────────────┘┴ ┴
typ ┴ └───────┘┴ └───────┘┴ └─────────────────────────┘┴ └┘┴
188 mem_range.2 (nat.lt_succ_of_le (nat.le_add_left _ _))⟩,
id └───────┘┴ └───────────────┘ └─────────────┘
src └───────┘┴ └───────────────┘ └─────────────┘
typ └───────┘┴ └───────────────┘ └─────────────┘
189 sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (nat.add_sub_cancel _ _).symm⟩⟩⟩)
id └──────────────┘┴ └─┘ └───────┘ └────────────────┘ └──┘
src └──────────────┘┴ └─┘ └───────┘ └────────────────┘ └──┘
typ └──────────────┘┴ └─┘ └───────┘ └────────────────┘ └──┘
190
191 lemma abv_sum_le_sum_abv {γ : Type*} (f : γ → β) (s : finset γ) :
id ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ └────┘ ┴
doc └────┘
192 abv (s.sum f) ≤ s.sum (abv ∘ f) :=
id └─┘ ┴└──┘ ┴ ┴ ┴└──┘ └─┘ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ └─┘ ┴└──┘ ┴ ┴ ┴└──┘ └─┘ ┴ ┴
193 by haveI := classical.dec_eq γ; exact
id └──────────────┘ ┴
src └───────┘└──────────────┘┴ └────┘
typ └───────┘└──────────────┘┴┴ └────┘
doc └───────┘ ┴ └────┘
txt └───────┘ ┴ └────┘
par └───────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └───────────────────────────────────
194 finset.induction_on s (by simp [abv_zero abv])
id └─────────────────┘ ┴ └──────┘ └─┘
src └─────────────────┘┴ ┴ ┴└────┘└──────┘┴ ┴└─
typ └─────────────────┘┴┴┴ ┴└────┘└──────┘┴└─┘┴└─
doc └─────────────────┘┴ ┴ ┴└────┘ ┴ ┴└─
txt ┴ ┴ ┴└────┘ ┴ ┴└─
par ┴ ┴ ┴└────┘ ┴ ┴└─
pid ┴ ┴ └─────┘ ┴ └──
st ────────────────────────┘└──────────────────┘└─
195 (λ a s has ih, by rw [sum_insert has, sum_insert has];
id └────────┘ └─┘ └────────┘ └─┘
src ─┘ └───────────┘ ┴└──┘└────────┘┴ └┘└────────┘┴ ┴└─
typ ─┘ └───────────┘ ┴└──┘└────────┘┴└─┘└┘└────────┘┴└─┘┴└─
doc ─┘ └───────────┘ ┴└──┘ ┴ └┘ ┴ ┴└─
txt ─┘ └───────────┘ ┴└──┘ ┴ └┘ ┴ ┴└─
par ─┘ └───────────┘ ┴└──┘ ┴ └┘ ┴ ┴└─
pid ─┘ └───────────┘ └───┘ ┴ └┘ ┴ └──
st ──────────────────┘└─────────────────┘└──────────────┘┴└─
196 exact le_trans (abv_add abv _ _) (add_le_add_left ih _))
id └──────┘ └─────┘ └─┘ └─────────────┘ └┘
src ─────────┘└──────┘┴ └─────┘┴ └────┘ └─────────────┘┴ └────
typ ─────────┘└──────┘┴ └─────┘┴└─┘└────┘ └─────────────┘┴└┘└────
doc ─────────┘ ┴ ┴ └────┘ ┴ └────
txt ─────────┘ ┴ ┴ └────┘ ┴ └────
par ─────────┘ ┴ ┴ └────┘ ┴ └────
pid ─────────┘ ┴ ┴ └────┘ ┴ └──┘└
st ──────────────────────────────────────────────────────────┘└─
197
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
198 lemma sum_range_sub_sum_range {α : Type*} [add_comm_group α] {f : ℕ → α}
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴
199 {n m : ℕ} (hnm : n ≤ m) : (range m).sum f - (range n).sum f =
id ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴
src ┴ ┴ └───┘ └─┘ ┴ └───┘ └─┘ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴
doc └───┘ └───┘
200 ((range m).filter (λ k, n ≤ k)).sum f :=
id └───┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └───┘ └────┘ ┴ └─┘
typ └───┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───┘ └────┘
201 begin
st └─────
202 rw [← sum_sdiff (@filter_subset _ (λ k, n ≤ k) _ (range m)),
id └───────┘ └───────────┘ ┴ ┴ └───┘ ┴
src └────┘└───────┘┴ └───────────┘└─┘ └──┘ ┴┴┴ └──┘ └───┘┴ └───
typ └────┘└───────┘┴ └───────────┘└─┘ └──┘┴┴┴┴ └──┘ └───┘┴┴└───
doc └────┘ ┴ └─┘ └──┘ ┴ ┴ └──┘ └───┘┴ └───
txt └────┘ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ └───
par └────┘ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ └───
pid └──┘ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ └───
st ────────────────────────────────────────────────────────────┘└─
203 sub_eq_iff_eq_add, ← eq_sub_iff_add_eq, add_sub_cancel'],
id └───────────────┘ └───────────────┘ └─────────────┘
src ───┘└───────────────┘└──┘└───────────────┘└┘└─────────────┘┴
typ ───┘└───────────────┘└──┘└───────────────┘└┘└─────────────┘┴
doc ───┘ └──┘ └┘ ┴
txt ───┘ └──┘ └┘ ┴
par ───┘ └──┘ └┘ ┴
pid ───┘ └──┘ └┘ ┴
st ────────────────────┘└───────────────────┘└───────────────┘└──
204 refine finset.sum_congr
id └──────────────┘
src └─────┘└──────────────┘└
typ └─────┘└──────────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ──────────────────────────
205 (finset.ext.2 $ λ a, ⟨λ h, by simp at *; finish,
id └────────┘
src ───┘ └────────┘└─┘ ┴ └──┘ └──┘ ┴└───────┘└┘└────┘└─
typ ───┘ └────────┘└─┘ ┴ └──┘ └──┘ ┴└───────┘└┘└────┘└─
doc ───┘ └─┘ ┴ └──┘ └──┘ ┴└───────┘└┘└────┘└─
txt ───┘ └─┘ ┴ └──┘ └──┘ ┴└───────┘└┘└────┘└─
par ───┘ └─┘ ┴ └──┘ └──┘ ┴└───────┘└┘└────┘└─
pid ───┘ └─┘ ┴ └──┘ └──┘ └───────────────────
st ────────────────────────────────┘└────────────────┘└─
206 λ h, have ham : a < m := lt_of_lt_of_le (mem_range.1 h) hnm,
id ┴ ┴ └────────────┘ └───────┘ └─┘
src ───┘ └──┘ └─────┘ ┴┴┴ └──┘└────────────┘┴ └───────┘└─┘ └┘ └─
typ ───┘ └──┘ └─────┘ ┴┴┴┴└──┘└────────────┘┴ └───────┘└─┘ └┘└─┘└─
doc ───┘ └──┘ └─────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ └─
txt ───┘ └──┘ └─────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ └─
par ───┘ └──┘ └─────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ └─
pid ───┘ └──┘ └─────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ └─
st ─────────────────────────────────────────────────────────────────
207 by simp * at *⟩)
src ─────┘ ┴└─────────┘└──
typ ─────┘ ┴└─────────┘└──
doc ─────┘ ┴└─────────┘└──
txt ─────┘ ┴└─────────┘└──
par ─────┘ ┴└─────────┘└──
pid ─────┘ └──────────────
st ───────┘└──────────┘└──
208 (λ _ _, rfl),
id └─┘
src ───┘ └────┘└─┘┴
typ ───┘ └────┘└─┘┴
doc ───┘ └────┘ ┴
txt ───┘ └────┘ ┴
par ───┘ └────┘ ┴
pid ───┘ └────┘ ┴
st ───────────────┘└─
209 end
st ──┘
210
211 lemma cauchy_product {a b : ℕ → β}
id ┴ ┴
src ┴
typ ┴ ┴
212 (ha : is_cau_seq abs (λ m, (range m).sum (λ n, abv (a n))))
id └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └─┘ ┴ ┴
src └────────┘ └─┘ └───┘ └─┘
typ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └─┘ ┴ ┴
doc └────────┘ └───┘
213 (hb : is_cau_seq abv (λ m, (range m).sum b)) (ε : α) (ε0 : 0 < ε) :
id └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └────────┘ └───┘ └─┘ ┴
typ └────────┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └────────┘ └───┘
214 ∃ i : ℕ, ∀ j ≥ i, abv ((range j).sum a * (range j).sum b -
id ┴ ┴┴ ┴ ┴ └─┘ └───┘ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴
src ┴ ┴┴ └───┘ └─┘ ┴ └───┘ └─┘ ┴
typ ┴ ┴┴ ┴ ┴ └─┘ └───┘ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴
doc └───┘ └───┘
215 (range j).sum (λ n, (range (n + 1)).sum (λ m, a m * b (n - m)))) < ε :=
id └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └─┘ └───┘ ┴ └─┘ ┴ ┴ ┴
typ └───┘ ┴ └─┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
216 let ⟨Q, hQ⟩ := cau_seq.bounded ⟨_, hb⟩ in
id └─┘ ┴ └┘ └─────────────┘ └┘
src └─────────────┘
typ └─┘ ┴ └┘ └─────────────┘ └┘
217 let ⟨P, hP⟩ := cau_seq.bounded ⟨_, ha⟩ in
id └─┘ ┴ └┘ └─────────────┘ └┘
src └─────────────┘
typ └─┘ ┴ └┘ └─────────────┘ └┘
218 have hP0 : 0 < P, from lt_of_le_of_lt (abs_nonneg _) (hP 0),
id ┴ └────────────┘ └────────┘
src ┴ └────────────┘ └────────┘
typ ┴ └────────────┘ └────────┘
219 have hPε0 : 0 < ε / (2 * P),
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
220 from div_pos ε0 (mul_pos (show (2 : α) > 0, from by norm_num) hP0),
id └─────┘ └┘ └─────┘ ┴ ┴ └─┘
src └─────┘ └─────┘ ┴ └──────┘
typ └─────┘ └┘ └─────┘ ┴ ┴ └──────┘ └─┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
221 let ⟨N, hN⟩ := cau_seq.cauchy₂ ⟨_, hb⟩ hPε0 in
id └─┘ ┴ └┘ └─────────────┘ └┘ └──┘
src └─────────────┘
typ └─┘ ┴ └┘ └─────────────┘ └┘ └──┘
222 have hQε0 : 0 < ε / (4 * Q),
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
223 from div_pos ε0 (mul_pos (show (0 : α) < 4, by norm_num) (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))),
id └─────┘ └┘ └─────┘ ┴ ┴ └────────────┘ └────────┘
src └─────┘ └─────┘ ┴ └──────┘ └────────────┘ └────────┘
typ └─────┘ └┘ └─────┘ ┴ ┴ └──────┘ └────────────┘ └────────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
224 let ⟨M, hM⟩ := cau_seq.cauchy₂ ⟨_, ha⟩ hQε0 in
id └─┘ ┴ └─────────────┘ └┘ └──┘
src └─────────────┘
typ └─┘ ┴ └─────────────┘ └┘ └──┘
225 ⟨2 * (max N M + 1), λ K hK,
id ┴ └─┘ ┴ ┴ └┘
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ └┘
226 have h₁ : sum (range K) (λ m, (range (m + 1)).sum (λ k, a k * b (m - k))) =
id └─┘ └───┘ ┴ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └───┘ └───┘ ┴ └─┘ ┴ ┴ ┴
typ └─┘ └───┘ ┴ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
227 sum (range K) (λ m, sum (range (K - m)) (λ n, a m * b n)),
id └─┘ └───┘ ┴ ┴ └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └───┘ └─┘ └───┘ ┴ ┴
typ └─┘ └───┘ ┴ ┴ └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
228 by simpa using sum_range_diag_flip K (λ m n, a m * b n),
id └─────────────────┘ ┴ ┴ ┴ ┴
src └──────────┘└─────────────────┘┴ ┴ └────┘ ┴ ┴┴┴ ┴ ┴
typ └──────────┘└─────────────────┘┴┴┴ └────┘┴┴ ┴┴┴┴┴ ┴
doc └──────────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
txt └──────────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
par └──────────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴└────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
st └───────────────────────────────────────────────────┘
229 have h₂ : (λ i, (range (K - i)).sum (λ k, a i * b k)) = (λ i, a i * (range (K - i)).sum b),
id ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴
src └───┘ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ └─┘
typ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴
doc └───┘ └───┘
230 by simp [finset.mul_sum],
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └────────────────────┘
231 have h₃ : (range K).sum (λ i, a i * (range (K - i)).sum b) =
id └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └───┘ └─┘ ┴ └───┘ ┴ └─┘ ┴
typ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └───┘ └───┘
232 (range K).sum (λ i, a i * ((range (K - i)).sum b - (range K).sum b))
id └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴
src └───┘ └─┘ ┴ └───┘ ┴ └─┘ ┴ └───┘ └─┘
typ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴
doc └───┘ └───┘ └───┘
233 + (range K).sum (λ i, a i * (range K).sum b),
id ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴
src ┴ └───┘ └─┘ ┴ └───┘ └─┘
typ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴
doc └───┘ └───┘
234 by rw ← sum_add_distrib; simp [(mul_add _ _ _).symm],
id └─────────────┘ └─────┘
src └───┘└─────────────┘ └────┘ └─────┘└───────────┘
typ └───┘└─────────────┘ └────┘ └─────┘└───────────┘
doc └───┘ └────┘ └───────────┘
txt └───┘ └────┘ └───────────┘
par └───┘ └────┘ └───────────┘
pid └─┘ ┴┴ └───────────┘
st └────────────────────────────────────────────────┘
235 have two_mul_two : (4 : α) = 2 * 2, by norm_num,
id ┴ ┴ ┴
src ┴ ┴ └──────┘
typ ┴ ┴ ┴ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
236 have hQ0 : Q ≠ 0, from λ h, by simpa [h, lt_irrefl] using hQε0,
id ┴ ┴ ┴ └───────┘ └──┘
src ┴ └─────┘ └┘└───────┘└──────┘
typ ┴ ┴ └─────┘┴└┘└───────┘└──────┘└──┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └──────────────────────────────┘
237 have h2Q0 : 2 * Q ≠ 0, from mul_ne_zero two_ne_zero hQ0,
id ┴ ┴ └─────────┘ └─────────┘ └─┘
src ┴ ┴ └─────────┘ └─────────┘
typ ┴ ┴ └─────────┘ └─────────┘ └─┘
238 have hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
239 by rw [← div_div_eq_div_mul, div_mul_cancel _ (ne.symm (ne_of_lt hP0)),
id └────────────────┘ └────────────┘ └─────┘ └──────┘ └─┘
src └────┘└────────────────┘└┘└────────────┘└─┘ └─────┘┴ └──────┘┴ └───
typ └────┘└────────────────┘└┘└────────────┘└─┘ └─────┘┴ └──────┘┴└─┘└───
doc └────┘ └┘ └─┘ ┴ ┴ └───
txt └────┘ └┘ └─┘ ┴ ┴ └───
par └────┘ └┘ └─┘ ┴ ┴ └───
pid └──┘ └┘ └─┘ ┴ ┴ └───
st └───────────────────────┘└─────────────────────────────────────────┘└─
240 two_mul_two, mul_assoc, ← div_div_eq_div_mul, div_mul_cancel _ h2Q0, add_halves],
id └─────────┘ └───────┘ └────────────────┘ └────────────┘ └──┘ └────────┘
src ───┘ └┘└───────┘└──┘└────────────────┘└┘└────────────┘└─┘ └┘└────────┘┴
typ ───┘└─────────┘└┘└───────┘└──┘└────────────────┘└┘└────────────┘└─┘└──┘└┘└────────┘┴
doc ───┘ └┘ └──┘ └┘ └─┘ └┘ ┴
txt ───┘ └┘ └──┘ └┘ └─┘ └┘ ┴
par ───┘ └┘ └──┘ └┘ └─┘ └┘ ┴
pid ───┘ └┘ └──┘ └┘ └─┘ └┘ ┴
st ──────────────┘└─────────┘└────────────────────┘└─────────────────────┘└──────────┘┴
241 have hNMK : max N M + 1 < K,
id └─┘ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴
242 from lt_of_lt_of_le (by rw two_mul; exact lt_add_of_pos_left _ (nat.succ_pos _)) hK,
id └────────────┘ └─────┘ └────────────────┘ └──────────┘ └┘
src └────────────┘ └─┘└─────┘ └────┘└────────────────┘└─┘ └──────────┘└─┘
typ └────────────┘ └─┘└─────┘ └────┘└────────────────┘└─┘ └──────────┘└─┘ └┘
doc └─┘ └────┘ └─┘ └─┘
txt └─┘ └────┘ └─┘ └─┘
par └─┘ └────┘ └─┘ └─┘
pid ┴ ┴ └─┘ └─┘
st └──────────────────────────────────────────────────────┘
243 have hKN : N < K,
id ┴ ┴
src ┴
typ ┴ ┴
244 from calc N ≤ max N M : le_max_left _ _
id └─┘ └─────────┘
src └─┘ └─────────┘
typ └─┘ └─────────┘
245 ... < max N M + 1 : nat.lt_succ_self _
id └─┘ ┴ └──────────────┘
src └─┘ ┴ └──────────────┘
typ └─┘ ┴ └──────────────┘
246 ... < K : hNMK,
id ┴ └──┘
typ ┴ └──┘
247 have hsumlesum : (range (max N M + 1)).sum (λ i, abv (a i) *
id └───┘ └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
src └───┘ └─┘ ┴ └─┘ ┴
typ └───┘ └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
doc └───┘
248 abv ((range (K - i)).sum b - (range K).sum b)) ≤ (range (max N M + 1)).sum
id └─┘ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └───┘ └─┘ ┴ └─┘
src └───┘ ┴ └─┘ ┴ └───┘ └─┘ ┴ └───┘ └─┘ ┴ └─┘
typ └─┘ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └───┘ └─┘ ┴ └─┘
doc └───┘ └───┘ └───┘
249 (λ i, abv (a i) * (ε / (2 * P))),
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
250 from sum_le_sum (λ m hmJ, mul_le_mul_of_nonneg_left
id └────────┘ ┴ └─┘ └───────────────────────┘
src └────────┘ └───────────────────────┘
typ └────────┘ ┴ └─┘ └───────────────────────┘
251 (le_of_lt (hN (K - m) K
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴
252 (nat.le_sub_left_of_add_le (le_trans
id └───────────────────────┘ └──────┘
src └───────────────────────┘ └──────┘
typ └───────────────────────┘ └──────┘
253 (by rw two_mul; exact add_le_add (le_of_lt (mem_range.1 hmJ))
id └─────┘ └────────┘ └───────┘ └─┘
src └─┘└─────┘ └────┘└────────┘┴ ┴ └───────┘└─┘ └──
typ └─┘└─────┘ └────┘└────────┘┴ ┴ └───────┘└─┘└─┘└──
doc └─┘ └────┘ ┴ ┴ └─┘ └──
txt └─┘ └────┘ ┴ ┴ └─┘ └──
par └─┘ └────┘ ┴ ┴ └─┘ └──
pid ┴ ┴ ┴ ┴ └─┘ └──
st └──────────────────────────────────────────────────────────
254 (le_trans (le_max_left _ _) (le_of_lt (lt_add_one _)))) hK))
id └──────┘ └─────────┘ └──────┘ └────────┘ └┘
src ─────────┘ └──────┘┴ └─────────┘└────┘ └──────┘┴ └────────┘└───┘
typ ─────────┘ └──────┘┴ └─────────┘└────┘ └──────┘┴ └────────┘└───┘ └┘
doc ─────────┘ ┴ └────┘ ┴ └───┘
txt ─────────┘ ┴ └────┘ ┴ └───┘
par ─────────┘ ┴ └────┘ ┴ └───┘
pid ─────────┘ ┴ └────┘ ┴ └───┘
st ───────────────────────────────────────────────────────────────┘
255 (le_of_lt hKN))) (abv_nonneg abv _)),
id └──────┘ └─┘ └────────┘ └─┘
src └──────┘ └────────┘
typ └──────┘ └─┘ └────────┘ └─┘
256 have hsumltP : sum (range (max N M + 1)) (λ n, abv (a n)) < P :=
id └─┘ └───┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ └───┘ └─┘ ┴ ┴
typ └─┘ └───┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───┘
257 calc sum (range (max N M + 1)) (λ n, abv (a n))
id └─┘ └───┘ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └───┘ └─┘ ┴
typ └─┘ └───┘ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └───┘
258 = abs (sum (range (max N M + 1)) (λ n, abv (a n))) :
id └─┘ └─┘ └───┘ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘ └───┘ └─┘ ┴
typ └─┘ └─┘ └───┘ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └───┘
259 eq.symm (abs_of_nonneg (sum_nonneg (λ x h, abv_nonneg abv (a x))))
id └─────┘ └───────────┘ └────────┘ ┴ ┴ └────────┘ └─┘ ┴ ┴
src └─────┘ └───────────┘ └────────┘ └────────┘
typ └─────┘ └───────────┘ └────────┘ ┴ ┴ └────────┘ └─┘ ┴ ┴
260 ... < P : hP (max N M + 1),
id └─┘ ┴
src └─┘ ┴
typ └─┘ ┴
261 begin
st └─────
262 rw [h₁, h₂, h₃, sum_mul, ← sub_sub, sub_right_comm, sub_self, zero_sub, abv_neg abv],
id └┘ └┘ └┘ └─────┘ └─────┘ └────────────┘ └──────┘ └──────┘ └─────┘ └─┘
src └──┘ └┘ └┘ └┘└─────┘└──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└─────┘┴ ┴
typ └──┘└┘└┘└┘└┘└┘└┘└─────┘└──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└─────┘┴└─┘┴
doc └──┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴ ┴
txt └──┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴ ┴
par └──┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴ ┴
pid └┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴ ┴
st ───────┘└──┘└──┘└───────┘└─────────┘└──────────────┘└────────┘└────────┘└───────────┘└──
263 refine lt_of_le_of_lt (abv_sum_le_sum_abv _ _) _,
id └────────────┘ └────────────────┘
src └─────┘└────────────┘┴ └────────────────┘└─────┘
typ └─────┘└────────────┘┴ └────────────────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ─────────────────────────────────────────────────┘└─
264 suffices : (range (max N M + 1)).sum (λ (i : ℕ), abv (a i) * abv ((range (K - i)).sum b - (range K).sum b)) +
id ┴ ┴
src └─────────┘ ┴ ┴ ┴ ┴┴└───────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ └
typ └─────────┘ ┴ ┴ ┴ ┴┴└───────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ └
doc └─────────┘ ┴ ┴ ┴ ┴ └───────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ └
txt └─────────┘ ┴ ┴ ┴ ┴ └───────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ └
par └─────────┘ ┴ ┴ ┴ ┴ └───────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ └
pid └───────┘└┘ ┴ ┴ ┴ ┴ └───────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ └
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────────
265 ((range K).sum (λ (i : ℕ), abv (a i) * abv ((range (K - i)).sum b - (range K).sum b)) -(range (max N M + 1)).sum
id └─┘ ┴ ┴
src ───┘ ┴ └────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ └─┘┴ ┴ ┴ └────────
typ ───┘ ┴ └────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ └─┘┴┴┴┴┴ └────────
doc ───┘ ┴ └────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └────────
txt ───┘ ┴ └────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └────────
par ───┘ ┴ └────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └────────
pid ───┘ ┴ └────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └────────
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
266 (λ (i : ℕ), abv (a i) * abv ((range (K - i)).sum b - (range K).sum b))) < ε / (2 * P) * P + ε / (4 * Q) * (2 * Q),
id ┴ └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───┘┴ └────┘ └──┘┴┴ ┴┴┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
typ ────┘ └────┘ └─┘ ┴ ┴┴ └┘ ┴└─┘┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───┘┴┴└────┘┴└──┘┴┴ ┴┴┴ └┘ ┴ └┘ ┴┴┴ ┴┴┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴┴
doc ────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───┘┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
txt ────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
par ────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
pid ────┘ └────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
267 { rw hε at this, simpa [abv_mul abv] },
id └┘ └─────┘ └─┘
src └─┘ └──────┘ └─────┘└─────┘┴ └┘
typ └─┘└┘└──────┘ └─────┘└─────┘┴└─┘└┘
doc └─┘ └──────┘ └─────┘ ┴ └┘
txt └─┘ └──────┘ └─────┘ ┴ └┘
par └─┘ └──────┘ └─────┘ ┴ └┘
pid ┴ └──────┘ ┴┴ ┴ ┴┴
st ───┘└───────────┘└────────────────────┘└┘└
268 refine add_lt_add (lt_of_le_of_lt hsumlesum
id └────────┘ └────────────┘ └───────┘
src └─────┘└────────┘┴ └────────────┘┴ └
typ └─────┘└────────┘┴ └────────────┘┴└───────┘└
doc └─────┘ ┴ ┴ └
txt └─────┘ ┴ ┴ └
par └─────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ──────────────────────────────────────────────
269 (by rw [← sum_mul, mul_comm]; exact (mul_lt_mul_left hPε0).mpr hsumltP)) _,
id └─────┘ └──────┘ └─────────────┘ └──┘ └─────┘
src ───┘ ┴└────┘└─────┘└┘└──────┘┴└┘└────┘ └─────────────┘┴ └────┘ └──┘
typ ───┘ ┴└────┘└─────┘└┘└──────┘┴└──────┘ └─────────────┘┴└──┘└────┘└─────┘└──┘
doc ───┘ ┴└────┘ └┘ ┴└┘└────┘ ┴ └────┘ └──┘
txt ───┘ ┴└────┘ └┘ ┴└┘└────┘ ┴ └────┘ └──┘
par ───┘ ┴└────┘ └┘ ┴└──────┘ ┴ └────┘ └──┘
pid ───┘ └─────┘ └┘ └───────┘ ┴ └────┘ └──┘
st ──────┘└────────────┘└────────┘┴└────────────────────────────────────────┘└──┘└─
270 rw sum_range_sub_sum_range (le_of_lt hNMK),
id └─────────────────────┘ └──────┘ └──┘
src └─┘└─────────────────────┘┴ └──────┘┴ ┴
typ └─┘└─────────────────────┘┴ └──────┘┴└──┘┴
doc └─┘ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────┘└─
271 exact calc sum ((range K).filter (λ k, max N M + 1 ≤ k))
id ┴
src └────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘┴┴ └──
typ └────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘┴┴ └──
doc └────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └──
txt └────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └──
par └────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └──
pid ┴ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └──
st ───────────────────────────────────────────────────────────
272 (λ i, abv (a i) * abv (sum (range (K - i)) b - sum (range K) b))
id ┴
src ─────┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──
typ ─────┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘┴└──
doc ─────┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──
txt ─────┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──
par ─────┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──
pid ─────┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──
st ───────────────────────────────────────────────────────────────────────
273 ≤ sum ((range K).filter (λ k, max N M + 1 ≤ k)) (λ i, abv (a i) * (2 * Q)) :
id └─┘ └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src ─────┘ ┴└─┘┴ └───┘┴ └───────┘ └──┘└─┘┴ ┴ ┴ └─┘ ┴ └─┘ └──┘ ┴ ┴ └┘ ┴ └┘ ┴ └────
typ ─────┘ ┴└─┘┴ └───┘┴┴└───────┘ └──┘└─┘┴┴┴┴┴ └─┘ ┴ └─┘ └──┘└─┘┴ ┴┴ └┘ ┴ └┘ ┴ └────
doc ─────┘ ┴ ┴ └───┘┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └──┘ ┴ ┴ └┘ ┴ └┘ ┴ └────
txt ─────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └──┘ ┴ ┴ └┘ ┴ └┘ ┴ └────
par ─────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └──┘ ┴ ┴ └┘ ┴ └┘ ┴ └────
pid ─────┘ ┴ ┴ ┴ └───────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ └─┘ └──┘ ┴ ┴ └┘ ┴ └┘ ┴ └────
st ───────────────────────────────────────────────────────────────────────────────────
274 sum_le_sum (λ n hn, begin
id └────────┘
src ───┘└────────┘┴ └─────┘ └
typ ───┘└────────┘┴ └─────┘ └
doc ───┘ ┴ └─────┘ └
txt ───┘ ┴ └─────┘ └
par ───┘ ┴ └─────┘ └
pid ───┘ ┴ └─────┘ └
st ───────────────────────┘└─────
275 refine mul_le_mul_of_nonneg_left _ (abv_nonneg _ _),
id └───────────────────────┘ └────────┘
src ─────┘└─────┘└───────────────────────┘└─┘ └────────┘└───┘└─
typ ────────────┘└───────────────────────┘└─┘ └────────┘└──────
doc ─────┘└─────┘ └─┘ └───┘└─
txt ─────┘└─────┘ └─┘ └───┘└─
par ────────────┘ └─┘ └──────
pid ────────────┘ └─┘ └──────
st ────────────────────────────────────────────────────────┘└─
276 rw sub_eq_add_neg,
id └────────────┘
src ─────┘└─┘└────────────┘└─
typ ─────┘└─┘└────────────┘└─
doc ─────┘└─┘ └─
txt ─────┘└─┘ └─
par ─────┘└─┘ └─
pid ────────┘ └─
st ──────────────────────┘└─
277 refine le_trans (abv_add _ _ _) _,
id └──────┘ └─────┘
src ─────┘└─────┘└──────┘┴ └─────┘└───────┘└─
typ ────────────┘└──────┘┴ └─────┘└──────────
doc ─────┘└─────┘ ┴ └───────┘└─
txt ─────┘└─────┘ ┴ └───────┘└─
par ────────────┘ ┴ └──────────
pid ────────────┘ ┴ └──────────
st ──────────────────────────────────────┘└─
278 rw [two_mul, abv_neg abv],
id └─┘
src ─────┘└──┘
typ ─────┘└──┘ └─┘
doc ─────┘└──┘
txt ─────┘└──┘
par ─────┘└──┘
pid ─────────┘
st ─────────┘
279 exact add_le_add (le_of_lt (hQ _)) (le_of_lt (hQ _)),
280 end)
st └─┘
281 ... < ε / (4 * Q) * (2 * Q) :
id ┴ ┴
typ ┴ ┴
282 by rw [← sum_mul, ← sum_range_sub_sum_range (le_of_lt hNMK)];
283 refine (mul_lt_mul_right $ by rw two_mul;
284 exact add_pos (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))
285 (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0))).2
286 (lt_of_le_of_lt (le_abs_self _)
287 (hM _ _ (le_trans (nat.le_succ_of_le (le_max_right _ _)) (le_of_lt hNMK))
288 (nat.le_succ_of_le (le_max_right _ _))))
289 end⟩
st └─┘
290
291 end
292
293 open finset
294
295 open cau_seq
296
297 namespace complex
298
299 lemma is_cau_abs_exp (z : ℂ) : is_cau_seq _root_.abs
id ┴
src ┴
typ ┴
300 (λ n, (range n).sum (λ m, abs (z ^ m / nat.fact m))) :=
id ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴
src └┘ └┘ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴
doc └┘ └┘
301 let ⟨n, hn⟩ := exists_nat_gt (abs z) in
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
302 have hn0 : (0 : ℝ) < n, from lt_of_le_of_lt (abs_nonneg _) hn,
id ┴
src ┴
typ ┴
303 series_ratio_test n (complex.abs z / n) (div_nonneg_of_nonneg_of_pos (complex.abs_nonneg _) hn0)
id └──┘ └─┘ ┴
src └──┘ └─┘
typ └──┘ └─┘ ┴
304 (by rwa [div_lt_iff hn0, one_mul])
305 (λ m hm,
id ┴ └┘
typ ┴ └┘
306 by rw [abs_abs, abs_abs, nat.fact_succ, pow_succ,
307 mul_comm m.succ, nat.cast_mul, ← div_div_eq_div_mul, mul_div_assoc,
id └────┘
src └────┘
typ └────┘
308 mul_div_right_comm, abs_mul, abs_div, abs_cast_nat];
309 exact mul_le_mul_of_nonneg_right
310 (div_le_div_of_le_left (abs_nonneg _) hn0
311 (nat.cast_le.2 (le_trans hm (nat.le_succ _)))) (abs_nonneg _))
id └┘
typ └┘
312
313 noncomputable theory
314
315 lemma is_cau_exp (z : ℂ) : is_cau_seq abs (λ n, (range n).sum (λ m, z ^ m / nat.fact m)) :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
src ┴ └┘ └┘ └┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴
doc └┘ └┘
316 is_cau_series_of_abv_cau (is_cau_abs_exp z)
id ┴
typ ┴
317
318 def exp' (z : ℂ) : cau_seq ℂ complex.abs := ⟨λ n, (range n).sum (λ m, z ^ m / nat.fact m), is_cau_exp z⟩
id ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
src ┴ └┘ └┘ └┘ └┘ └┘ ┴
typ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
doc └┘ └┘ ┴
319
320 def exp (z : ℂ) : ℂ := lim (exp' z)
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
321
322 def sin (z : ℂ) : ℂ := ((exp (-z * I) - exp (z * I)) * I) / 2
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
323
324 def cos (z : ℂ) : ℂ := (exp (z * I) + exp (-z * I)) / 2
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
325
326 def tan (z : ℂ) : ℂ := sin z / cos z
id ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘ ┴
327
328 def sinh (z : ℂ) : ℂ := (exp z - exp (-z)) / 2
id ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘ ┴
329
330 def cosh (z : ℂ) : ℂ := (exp z + exp (-z)) / 2
id ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘ ┴
331
332 def tanh (z : ℂ) : ℂ := sinh z / cosh z
id ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴
333
334 end complex
335
336 namespace real
337
338 open complex
339
340 def exp (x : ℝ) : ℝ := (exp x).re
id ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
341
342 def sin (x : ℝ) : ℝ := (sin x).re
id ┴ ┴ └┘ ┴ ┴
src ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴ ┴
343
344 def cos (x : ℝ) : ℝ := (cos x).re
id ┴ ┴ └┘ ┴ ┴
src ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴ ┴
345
346 def tan (x : ℝ) : ℝ := (tan x).re
id ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
347
348 def sinh (x : ℝ) : ℝ := (sinh x).re
id ┴ ┴ └┘ ┴ └┘
src ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ ┴ └┘
349
350 def cosh (x : ℝ) : ℝ := (cosh x).re
id ┴ ┴ └┘ ┴ └┘
src ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ ┴ └┘
351
352 def tanh (x : ℝ) : ℝ := (tanh x).re
id ┴ ┴ └┘ ┴ └┘
src ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ ┴ └┘
353
354 end real
355
356 namespace complex
357
358 variables (x y : ℂ)
id ┴
src ┴
typ ┴
359
360 @[simp] lemma exp_zero : exp 0 = 1 :=
id └─┘ ┴
src └─┘ ┴
typ └─┘ ┴
doc └──┘
361 lim_eq_of_equiv_const $
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
362 λ ε ε0, ⟨1, λ j hj, begin
id ┴ └┘ ┴ └┘
typ ┴ └┘ ┴ └┘
st └─────
363 convert ε0,
id └┘
src └──────┘
typ └──────┘└┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───────────┘└─
364 cases j,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────┘└─
365 { exact absurd hj (not_le_of_gt zero_lt_one) },
id └────┘ └┘ └──────────┘ └─────────┘
src └────┘└────┘┴ ┴ └──────────┘┴└─────────┘└┘
typ └────┘└────┘┴└┘┴ └──────────┘┴└─────────┘└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ───┘└─────────────────────────────────────────┘└┘└
366 { dsimp [exp'],
id └──┘
src └─────┘└──┘┴
typ └─────┘└──┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ───────────────┘└─
367 induction j with j ih,
id ┴
typ ┴
st ───┘ ┴
368 { dsimp [exp']; simp },
st ┴
369 { rw ← ih dec_trivial,
370 simp only [sum_range_succ, pow_succ],
371 simp } }
st └───
372 end⟩
st ──┘
373
374 lemma exp_add : exp (x + y) = exp x * exp y :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
375 show lim (⟨_, is_cau_exp (x + y)⟩ : cau_seq ℂ abs) =
id └─┘ └────────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
src └─┘ └────────┘ ┴ └─────┘ ┴ └─┘
typ └─┘ └────────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
376 lim (show cau_seq ℂ abs, from ⟨_, is_cau_exp x⟩)
id └─┘ └─────┘ ┴ └─┘ └────────┘ ┴
src └─┘ └─────┘ ┴ └─┘ └────────┘
typ └─┘ └─────┘ ┴ └─┘ └────────┘ ┴
377 * lim (show cau_seq ℂ abs, from ⟨_, is_cau_exp y⟩),
id ┴ └─┘ └─────┘ ┴ └─┘ └────────┘ ┴
src ┴ └─┘ └─────┘ ┴ └─┘ └────────┘
typ ┴ └─┘ └─────┘ ┴ └─┘ └────────┘ ┴
378 from
379 have hj : ∀ j : ℕ, (range j).sum
id ┴ └───┘ ┴ └─┘
src ┴ └───┘ └─┘
typ ┴ └───┘ ┴ └─┘
doc └───┘
380 (λ m, (x + y) ^ m / m.fact) = (range j).sum
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ └───┘ ┴ └─┘
src ┴ ┴ ┴ └───┘ ┴ └───┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ └───┘ ┴ └─┘
doc └───┘ └───┘
381 (λ i, (range (i + 1)).sum (λ k, x ^ k / k.fact *
id ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └───┘ ┴ └─┘ ┴ ┴ └───┘ ┴
typ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └───┘ └───┘
382 (y ^ (i - k) / (i - k).fact))),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
383 from assume j,
id ┴
typ ┴
384 finset.sum_congr rfl (λ m hm, begin
id └──────────────┘ └─┘ ┴ └┘
src └──────────────┘ └─┘
typ └──────────────┘ └─┘ ┴ └┘
385 rw [add_pow, div_eq_mul_inv, sum_mul],
386 refine finset.sum_congr rfl (λ i hi, _),
387 have h₁ : (nat.choose m i : ℂ) ≠ 0 := nat.cast_ne_zero.2
388 (nat.pos_iff_ne_zero.1 (nat.choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
389 have h₂ := nat.choose_mul_fact_mul_fact (nat.le_of_lt_succ $ finset.mem_range.1 hi),
390 rw [← h₂, nat.cast_mul, nat.cast_mul, mul_inv', mul_inv'],
391 simp only [mul_left_comm (nat.choose m i : ℂ), mul_assoc, mul_left_comm (nat.choose m i : ℂ)⁻¹,
id └────────┘ ┴ ┴ └────────┘ ┴ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘ └────────┘
392 mul_comm (nat.choose m i : ℂ)],
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
doc └────────┘
393 rw inv_mul_cancel h₁,
394 simp [div_eq_mul_inv, mul_comm, mul_assoc, mul_left_comm]
395 end),
st └─┘
396 by rw lim_mul_lim;
397 exact eq.symm (lim_eq_lim_of_equiv (by dsimp; simp only [hj];
398 exact cauchy_product (is_cau_abs_exp x) (is_cau_exp y)))
id ┴ ┴
typ ┴ ┴
399
400 attribute [irreducible] complex.exp
id └────┘ └─┘
src └────┘ └─┘
typ └────┘ └─┘
doc └─────────┘
401
402 lemma exp_list_sum (l : list ℂ) : exp l.sum = (l.map exp).prod :=
id └┘ ┴ ┴ ┴ ┴ └┘
src └┘ ┴ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ └┘
403 @monoid_hom.map_list_prod (multiplicative ℂ) ℂ _ _ ⟨exp, exp_zero, exp_add⟩ l
id └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ ┴ ┴ └┘
typ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
404
405 lemma exp_multiset_sum (s : multiset ℂ) : exp s.sum = (s.map exp).prod :=
id └┘ └┘ ┴ ┴ ┴ ┴ └┘
src └┘ └┘ ┴ ┴ └┘
typ └┘ └┘ ┴ ┴ ┴ ┴ └┘
doc └┘ └┘
406 @monoid_hom.map_multiset_prod (multiplicative ℂ) ℂ _ _ ⟨exp, exp_zero, exp_add⟩ s
id └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ ┴ ┴ └┘
typ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴
407
408 lemma exp_sum {α : Type*} (s : finset α) (f : α → ℂ) : exp (s.sum f) = s.prod (exp ∘ f) :=
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ └┘ └┘
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
doc └┘
409 @monoid_hom.map_prod α (multiplicative ℂ) ℂ _ _ ⟨exp, exp_zero, exp_add⟩ f s
id ┴ └┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴
src └┘ └┘ └┘ └┘ ┴ └┘
typ ┴ └┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴
410
411 lemma exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp(n*x) = (exp x)^n
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
412 | 0 := by rw [nat.cast_zero, zero_mul, exp_zero, pow_zero]
st ┴
413 | (nat.succ n) := by rw [pow_succ', nat.cast_add_one, add_mul, exp_add, ←exp_nat_mul, one_mul]
id └──────┘
src └──────┘
typ └──────┘
st ┴
414
415 lemma exp_ne_zero : exp x ≠ 0 :=
id └┘ ┴
src └┘
typ └┘ ┴
416 λ h, @zero_ne_one ℂ _ $
id ┴
src ┴
typ ┴
417 by rw [← exp_zero, ← add_neg_self x, exp_add, h]; simp
418
419 lemma exp_neg : exp (-x) = (exp x)⁻¹ :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
420 by rw [← domain.mul_left_inj (exp_ne_zero x), ← exp_add];
421 simp [mul_inv_cancel (exp_ne_zero x)]
id ┴
typ ┴
422
423 lemma exp_sub : exp (x - y) = exp x / exp y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴
424 by simp [exp_add, exp_neg, div_eq_mul_inv]
425
426 @[simp] lemma exp_conj : exp (conj x) = conj (exp x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
doc └──┘
427 begin
428 dsimp [exp],
id └─┘
src └─┘
typ └─┘
429 rw [← lim_conj],
430 refine congr_arg lim (cau_seq.ext (λ _, _)),
id ┴
typ ┴
431 dsimp [exp', function.comp, cau_seq_conj],
432 rw ← sum_hom _ conj,
id └──┘
src └──┘
typ └──┘
433 refine sum_congr rfl (λ n hn, _),
id ┴
typ ┴
434 rw [conj_div, conj_pow, ← of_real_nat_cast, conj_of_real]
st ┴
435 end
st └─┘
436
437 @[simp] lemma of_real_exp_of_real_re (x : ℝ) : ((exp x).re : ℂ) = exp x :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
438 eq_conj_iff_re.1 $ by rw [← exp_conj, conj_of_real]
439
440 @[simp] lemma of_real_exp (x : ℝ) : (real.exp x : ℂ) = exp x :=
id ┴ └┘ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ ┴ └┘
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴
doc └──┘
441 of_real_exp_of_real_re _
442
443 @[simp] lemma exp_of_real_im (x : ℝ) : (exp x).im = 0 :=
id ┴ └┘ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴
doc └──┘
444 by rw [← of_real_exp_of_real_re, of_real_im]
445
446 lemma exp_of_real_re (x : ℝ) : (exp x).re = real.exp x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴
447
448 lemma two_sinh : 2 * sinh x = exp x - exp (-x) :=
id └┘ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ └┘ ┴ ┴ ┴
449 mul_div_cancel' _ two_ne_zero'
450
451 lemma two_cosh : 2 * cosh x = exp x + exp (-x) :=
id └┘ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ └┘ ┴ ┴ ┴
452 mul_div_cancel' _ two_ne_zero'
453
454 @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └──┘
455
456 @[simp] lemma sinh_neg : sinh (-x) = -sinh x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
457 by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]
id └──┘
src └──┘
typ └──┘
458
459 private lemma sinh_add_aux {a b c d : ℂ} :
id ┴
src ┴
typ ┴
460 (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d) := by ring
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
461
462 lemma sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
463 begin
464 rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_sinh,
465 exp_add, neg_add, exp_add, eq_comm,
466 mul_add, ← mul_assoc, two_sinh, mul_left_comm, two_sinh,
467 ← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_add,
468 mul_left_comm, two_cosh, ← mul_assoc, two_cosh],
469 exact sinh_add_aux
470 end
st └─┘
471
472 @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └──┘
473
474 @[simp] lemma cosh_neg : cosh (-x) = cosh x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
475 by simp [cosh, exp_neg]
id └──┘
src └──┘
typ └──┘
476
477 private lemma cosh_add_aux {a b c d : ℂ} :
id ┴
src ┴
typ ┴
478 (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d) := by ring
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
479
480 lemma cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
481 begin
482 rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_cosh,
483 exp_add, neg_add, exp_add, eq_comm,
484 mul_add, ← mul_assoc, two_cosh, ← mul_assoc, two_sinh,
485 ← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_add,
486 mul_left_comm, two_cosh, mul_left_comm, two_sinh],
487 exact cosh_add_aux
488 end
st └─┘
489
490 lemma sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
491 by simp [sinh_add, sinh_neg, cosh_neg]
492
493 lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
494 by simp [cosh_add, sinh_neg, cosh_neg]
495
496 lemma sinh_conj : sinh (conj x) = conj (sinh x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
497 by rw [sinh, ← conj_neg, exp_conj, exp_conj, ← conj_sub, sinh, conj_div, conj_two]
st ┴
498
499 @[simp] lemma of_real_sinh_of_real_re (x : ℝ) : ((sinh x).re : ℂ) = sinh x :=
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘
500 eq_conj_iff_re.1 $ by rw [← sinh_conj, conj_of_real]
501
502 @[simp] lemma of_real_sinh (x : ℝ) : (real.sinh x : ℂ) = sinh x :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
503 of_real_sinh_of_real_re _
504
505 @[simp] lemma sinh_of_real_im (x : ℝ) : (sinh x).im = 0 :=
id ┴ └┘ ┴ └┘
src ┴ └┘ └┘
typ ┴ └┘ ┴ └┘
doc └──┘
506 by rw [← of_real_sinh_of_real_re, of_real_im]
507
508 lemma sinh_of_real_re (x : ℝ) : (sinh x).re = real.sinh x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘ └┘ ┴
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴ ┴
509
510 lemma cosh_conj : cosh (conj x) = conj (cosh x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
511 by rw [cosh, ← conj_neg, exp_conj, exp_conj, ← conj_add, cosh, conj_div, conj_two]
st ┴
512
513 @[simp] lemma of_real_cosh_of_real_re (x : ℝ) : ((cosh x).re : ℂ) = cosh x :=
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘
514 eq_conj_iff_re.1 $ by rw [← cosh_conj, conj_of_real]
515
516 @[simp] lemma of_real_cosh (x : ℝ) : (real.cosh x : ℂ) = cosh x :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
517 of_real_cosh_of_real_re _
518
519 @[simp] lemma cosh_of_real_im (x : ℝ) : (cosh x).im = 0 :=
id ┴ └┘ ┴ └┘
src ┴ └┘ └┘
typ ┴ └┘ ┴ └┘
doc └──┘
520 by rw [← of_real_cosh_of_real_re, of_real_im]
521
522 lemma cosh_of_real_re (x : ℝ) : (cosh x).re = real.cosh x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘ └┘ ┴
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴ ┴
523
524 lemma tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x := rfl
id └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘
typ └┘ ┴ └┘ ┴ └┘ ┴
525
526 @[simp] lemma tanh_zero : tanh 0 = 0 := by simp [tanh]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └──┘
527
528 @[simp] lemma tanh_neg : tanh (-x) = -tanh x := by simp [tanh, neg_div]
id └┘ ┴ └┘ ┴ └──┘
src └┘ └┘ └──┘
typ └┘ ┴ └┘ ┴ └──┘
doc └──┘
529
530 lemma tanh_conj : tanh (conj x) = conj (tanh x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
531 by rw [tanh, sinh_conj, cosh_conj, ← conj_div, tanh]
st ┴
532
533 @[simp] lemma of_real_tanh_of_real_re (x : ℝ) : ((tanh x).re : ℂ) = tanh x :=
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘
534 eq_conj_iff_re.1 $ by rw [← tanh_conj, conj_of_real]
535
536 @[simp] lemma of_real_tanh (x : ℝ) : (real.tanh x : ℂ) = tanh x :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
537 of_real_tanh_of_real_re _
538
539 @[simp] lemma tanh_of_real_im (x : ℝ) : (tanh x).im = 0 :=
id ┴ └┘ ┴ └┘
src ┴ └┘ └┘
typ ┴ └┘ ┴ └┘
doc └──┘
540 by rw [← of_real_tanh_of_real_re, of_real_im]
541
542 lemma tanh_of_real_re (x : ℝ) : (tanh x).re = real.tanh x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘ └┘ ┴
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴ ┴
543
544 lemma cosh_add_sinh : cosh x + sinh x = exp x :=
id └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘
typ └┘ ┴ └┘ ┴ └┘ ┴
545 by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_add,
546 two_cosh, two_sinh, add_add_sub_cancel, two_mul]
st ┴
547
548 lemma sinh_add_cosh : sinh x + cosh x = exp x :=
id └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘
typ └┘ ┴ └┘ ┴ └┘ ┴
549 by rw [add_comm, cosh_add_sinh]
550
551 lemma cosh_sub_sinh : cosh x - sinh x = exp (-x) :=
id └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘
typ └┘ ┴ └┘ ┴ └┘ ┴
552 by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), mul_sub,
553 two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
st ┴
554
555 lemma cosh_sq_sub_sinh_sq : cosh x ^ 2 - sinh x ^ 2 = 1 :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
556 by rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_self, exp_zero]
st ┴
557
558 @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin]
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
doc └──┘
559
560 @[simp] lemma sin_neg : sin (-x) = -sin x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
561 by simp [sin, exp_neg, (neg_div _ _).symm, add_mul]
id └─┘
src └─┘
typ └─┘
562
563 lemma two_sin : 2 * sin x = (exp (-x * I) - exp (x * I)) * I :=
id └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
564 mul_div_cancel' _ two_ne_zero'
565
566 lemma two_cos : 2 * cos x = exp (x * I) + exp (-x * I) :=
id └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
567 mul_div_cancel' _ two_ne_zero'
568
569 lemma sinh_mul_I : sinh (x * I) = sin x * I :=
id ┴ ┴ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴
570 by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_sinh,
571 ← mul_assoc, two_sin, mul_assoc, I_mul_I, mul_neg_one,
572 neg_sub, neg_mul_eq_neg_mul]
st ┴
573
574 lemma cosh_mul_I : cosh (x * I) = cos x :=
id └┘ ┴ ┴ └┘ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ └┘ ┴
575 by rw [← domain.mul_left_inj (@two_ne_zero' ℂ _ _ _), two_cosh,
576 two_cos, neg_mul_eq_neg_mul]
st ┴
577
578 lemma sin_add : sin (x + y) = sin x * cos y + cos x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
579 by rw [← domain.mul_right_inj I_ne_zero, ← sinh_mul_I,
580 add_mul, add_mul, mul_right_comm, ← sinh_mul_I,
581 mul_assoc, ← sinh_mul_I, ← cosh_mul_I, ← cosh_mul_I, sinh_add]
st ┴
582
583 @[simp] lemma cos_zero : cos 0 = 1 := by simp [cos]
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
doc └──┘
584
585 @[simp] lemma cos_neg : cos (-x) = cos x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
586 by simp [cos, exp_neg]
id └─┘
src └─┘
typ └─┘
587
588 private lemma cos_add_aux {a b c d : ℂ} :
id ┴
src ┴
typ ┴
589 (a + b) * (c + d) - (b - a) * (d - c) * (-1) =
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴
590 2 * (a * c + b * d) := by ring
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
591
592 lemma cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
593 by rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I,
594 sinh_mul_I, sinh_mul_I, mul_mul_mul_comm, I_mul_I,
595 mul_neg_one, sub_eq_add_neg]
st ┴
596
597 lemma sin_sub : sin (x - y) = sin x * cos y - cos x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
598 by simp [sin_add, sin_neg, cos_neg]
599
600 lemma cos_sub : cos (x - y) = cos x * cos y + sin x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
601 by simp [cos_add, sin_neg, cos_neg]
602
603 lemma sin_conj : sin (conj x) = conj (sin x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
604 by rw [← domain.mul_right_inj I_ne_zero, ← sinh_mul_I,
605 ← conj_neg_I, ← conj_mul, ← conj_mul, sinh_conj,
606 mul_neg_eq_neg_mul_symm, sinh_neg, sinh_mul_I, mul_neg_eq_neg_mul_symm]
st ┴
607
608 @[simp] lemma of_real_sin_of_real_re (x : ℝ) : ((sin x).re : ℂ) = sin x :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
609 eq_conj_iff_re.1 $ by rw [← sin_conj, conj_of_real]
610
611 @[simp] lemma of_real_sin (x : ℝ) : (real.sin x : ℂ) = sin x :=
id ┴ └┘ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ ┴ └┘
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴
doc └──┘
612 of_real_sin_of_real_re _
613
614 @[simp] lemma sin_of_real_im (x : ℝ) : (sin x).im = 0 :=
id ┴ └┘ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴
doc └──┘
615 by rw [← of_real_sin_of_real_re, of_real_im]
616
617 lemma sin_of_real_re (x : ℝ) : (sin x).re = real.sin x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴
618
619 lemma cos_conj : cos (conj x) = conj (cos x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
620 by rw [← cosh_mul_I, ← conj_neg_I, ← conj_mul, ← cosh_mul_I,
621 cosh_conj, mul_neg_eq_neg_mul_symm, cosh_neg]
st ┴
622
623 @[simp] lemma of_real_cos_of_real_re (x : ℝ) : ((cos x).re : ℂ) = cos x :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
624 eq_conj_iff_re.1 $ by rw [← cos_conj, conj_of_real]
625
626 @[simp] lemma of_real_cos (x : ℝ) : (real.cos x : ℂ) = cos x :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
627 of_real_cos_of_real_re _
628
629 @[simp] lemma cos_of_real_im (x : ℝ) : (cos x).im = 0 :=
id ┴ └┘ ┴ └┘
src ┴ └┘ └┘
typ ┴ └┘ ┴ └┘
doc └──┘
630 by rw [← of_real_cos_of_real_re, of_real_im]
631
632 lemma cos_of_real_re (x : ℝ) : (cos x).re = real.cos x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴
633
634 @[simp] lemma tan_zero : tan 0 = 0 := by simp [tan]
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
doc └──┘
635
636 lemma tan_eq_sin_div_cos : tan x = sin x / cos x := rfl
id └┘ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └┘ ┴
637
638 @[simp] lemma tan_neg : tan (-x) = -tan x := by simp [tan, neg_div]
id └┘ ┴ └┘ ┴ └─┘
src └┘ └┘ └─┘
typ └┘ ┴ └┘ ┴ └─┘
doc └──┘
639
640 lemma tan_conj : tan (conj x) = conj (tan x) :=
id └┘ └┘ ┴ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ ┴ └┘ └┘ ┴
641 by rw [tan, sin_conj, cos_conj, ← conj_div, tan]
st ┴
642
643 @[simp] lemma of_real_tan_of_real_re (x : ℝ) : ((tan x).re : ℂ) = tan x :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
644 eq_conj_iff_re.1 $ by rw [← tan_conj, conj_of_real]
645
646 @[simp] lemma of_real_tan (x : ℝ) : (real.tan x : ℂ) = tan x :=
id ┴ └┘ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ ┴ └┘
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴
doc └──┘
647 of_real_tan_of_real_re _
648
649 @[simp] lemma tan_of_real_im (x : ℝ) : (tan x).im = 0 :=
id ┴ └┘ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴
doc └──┘
650 by rw [← of_real_tan_of_real_re, of_real_im]
651
652 lemma tan_of_real_re (x : ℝ) : (tan x).re = real.tan x := rfl
id ┴ └┘ ┴ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ ┴ └┘ └┘ └┘ ┴
653
654 lemma cos_add_sin_I : cos x + sin x * I = exp (x * I) :=
id └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
655 by rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]
st ┴
656
657 lemma cos_sub_sin_I : cos x - sin x * I = exp (-x * I) :=
id └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
658 by rw [← neg_mul_eq_neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]
st ┴
659
660 lemma sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
661 eq.trans
662 (by rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm])
st ┴
663 (cosh_sq_sub_sinh_sq (x * I))
id ┴ ┴
src ┴
typ ┴ ┴
664
665 lemma cos_two_mul' : cos (2 * x) = cos x ^ 2 - sin x ^ 2 :=
id └┘ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ └┘ ┴ ┴ ┴
666 by rw [two_mul, cos_add, ← pow_two, ← pow_two]
st ┴
667
668 lemma cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
669 by rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x),
670 ← sub_add, sub_add_eq_add_sub, two_mul]
st ┴
671
672 lemma sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
id └┘ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ └┘ ┴ ┴ ┴
673 by rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
st ┴
674
675 lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
676 by simp [cos_two_mul, div_add_div_same, mul_div_cancel_left, two_ne_zero', -one_div_eq_inv]
677
678 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
679 by { rw [←sin_sq_add_cos_sq x], simp }
st └┘
680
681 lemma exp_mul_I : exp (x * I) = cos x + sin x * I :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
682 (cos_add_sin_I _).symm
683
684 lemma exp_add_mul_I : exp (x + y * I) = exp x * (cos y + sin y * I) :=
id └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴
685 by rw [exp_add, exp_mul_I]
st ┴
686
687 lemma exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * I) :=
id └┘ ┴ ┴ ┴└─┘ └┘ ┴└┘ └┘ ┴ └┘ ┴
src └┘ ┴ └─┘ └┘ └┘ └┘ └┘ ┴
typ └┘ ┴ ┴ ┴└─┘ └┘ ┴└┘ └┘ ┴ └┘ ┴
688 by rw [← exp_add_mul_I, re_add_im]
689
690 theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) : (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
691 begin
692 rw [← exp_mul_I, ← exp_mul_I],
693 induction n with n ih,
id ┴
typ ┴
694 { rw [pow_zero, nat.cast_zero, zero_mul, zero_mul, exp_zero] },
st ┴ └┘
695 { rw [pow_succ', ih, nat.cast_succ, add_mul, add_mul, one_mul, exp_add] }
st ┴ └─
696 end
st ──┘
697
698 end complex
699
700 namespace real
701
702 open complex
703
704 variables (x y : ℝ)
id ┴
src ┴
typ ┴
705
706 @[simp] lemma exp_zero : exp 0 = 1 :=
id └─┘ ┴
src └─┘ ┴
typ └─┘ ┴
doc └──┘
707 by simp [real.exp]
id └──────┘
src └──────┘
typ └──────┘
st ┴ └──────┘
708
709 lemma exp_add : exp (x + y) = exp x * exp y :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
710 by simp [exp_add, exp]
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
st ┴ └─────┘ └─┘
711
712 lemma exp_list_sum (l : list ℝ) : exp l.sum = (l.map exp).prod :=
id └──┘ ┴ └─┘ ┴└──┘ ┴ ┴└──┘ └─┘ └──┘
src └──┘ ┴ └─┘ └──┘ ┴ └──┘ └─┘ └──┘
typ └──┘ ┴ └─┘ ┴└──┘ ┴ ┴└──┘ └─┘ └──┘
doc └──┘ └──┘
713 @monoid_hom.map_list_prod (multiplicative ℝ) ℝ _ _ ⟨exp, exp_zero, exp_add⟩ l
id └──────────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘ ┴
src └──────────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘
typ └──────────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘ ┴
714
715 lemma exp_multiset_sum (s : multiset ℝ) : exp s.sum = (s.map exp).prod :=
id └──────┘ ┴ └─┘ ┴└──┘ ┴ ┴└──┘ └─┘ └──┘
src └──────┘ ┴ └─┘ └──┘ ┴ └──┘ └─┘ └──┘
typ └──────┘ ┴ └─┘ ┴└──┘ ┴ ┴└──┘ └─┘ └──┘
doc └──────┘ └──┘ └──┘
716 @monoid_hom.map_multiset_prod (multiplicative ℝ) ℝ _ _ ⟨exp, exp_zero, exp_add⟩ s
id └──────────────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘ ┴
src └──────────────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘
typ └──────────────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘ ┴
717
718 lemma exp_sum {α : Type*} (s : finset α) (f : α → ℝ) : exp (s.sum f) = s.prod (exp ∘ f) :=
id └────┘ ┴ ┴ ┴ └─┘ ┴└──┘ ┴ ┴ ┴└───┘ └─┘ ┴ ┴
src └────┘ ┴ └─┘ └──┘ ┴ └───┘ └─┘ ┴
typ └────┘ ┴ ┴ ┴ └─┘ ┴└──┘ ┴ ┴ ┴└───┘ └─┘ ┴ ┴
doc └────┘ └───┘
719 @monoid_hom.map_prod α (multiplicative ℝ) ℝ _ _ ⟨exp, exp_zero, exp_add⟩ f s
id └─────────────────┘ ┴ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘ ┴ ┴
src └─────────────────┘ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘
typ └─────────────────┘ ┴ └────────────┘ ┴ ┴ └─┘ └──────┘ └─────┘ ┴ ┴
720
721 lemma exp_nat_mul (x : ℝ) : ∀ n : ℕ, exp(n*x) = (exp x)^n
id ┴ ┴ ┴ └─┘ ┴┴┴ ┴ └─┘ ┴ ┴┴
src ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴┴┴ ┴ └─┘ ┴ ┴┴
722 | 0 := by rw [nat.cast_zero, zero_mul, exp_zero, pow_zero]
id └───────────┘ └┘
src └───────────┘ └┘
typ └───────────┘ └┘
st ┴ └───────────┘ └┘ ┴
723 | (nat.succ n) := by rw [pow_succ', nat.cast_add_one, add_mul, exp_add, ←exp_nat_mul, one_mul]
id └──────┘
src └──────┘
typ └──────┘
st ┴
724
725 lemma exp_ne_zero : exp x ≠ 0 :=
id └┘ ┴
src └┘
typ └┘ ┴
726 λ h, exp_ne_zero x $ by rw [exp, ← of_real_inj] at h; simp * at *
id ┴
typ ┴
727
728 lemma exp_neg : exp (-x) = (exp x)⁻¹ :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
729 by rw [← of_real_inj, exp, of_real_exp_of_real_re, of_real_neg, exp_neg,
730 of_real_inv, of_real_exp]
st ┴
731
732 lemma exp_sub : exp (x - y) = exp x / exp y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴
733 by simp [exp_add, exp_neg, div_eq_mul_inv]
734
735 @[simp] lemma sin_zero : sin 0 = 0 := by simp [sin]
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
doc └──┘
736
737 @[simp] lemma sin_neg : sin (-x) = -sin x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
738 by simp [sin, exp_neg, (neg_div _ _).symm, add_mul]
id └─┘
src └─┘
typ └─┘
739
740 lemma sin_add : sin (x + y) = sin x * cos y + cos x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
741 by rw [← of_real_inj]; simp [sin, sin_add]
id └─┘
src └─┘
typ └─┘
742
743 @[simp] lemma cos_zero : cos 0 = 1 := by simp [cos]
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
doc └──┘
744
745 @[simp] lemma cos_neg : cos (-x) = cos x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
746 by simp [cos, exp_neg]
id └─┘
src └─┘
typ └─┘
747
748 lemma cos_add : cos (x + y) = cos x * cos y - sin x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
749 by rw ← of_real_inj; simp [cos, cos_add]
id └─┘
src └─┘
typ └─┘
750
751 lemma sin_sub : sin (x - y) = sin x * cos y - cos x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
752 by simp [sin_add, sin_neg, cos_neg]
753
754 lemma cos_sub : cos (x - y) = cos x * cos y + sin x * sin y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
755 by simp [cos_add, sin_neg, cos_neg]
756
757 lemma tan_eq_sin_div_cos : tan x = sin x / cos x :=
id └┘ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └┘ ┴
758 if h : complex.cos x = 0 then by simp [sin, cos, tan, *, complex.tan, div_eq_mul_inv] at *
id ┴ └─┘ └─┘ └─┘ └─────────┘
src └─┘ └─┘ └─┘ └─────────┘
typ ┴ └─┘ └─┘ └─┘ └─────────┘
759 else
760 by rw [sin, cos, tan, complex.tan, ← of_real_inj, div_eq_mul_inv, mul_re];
761 simp [norm_sq, (div_div_eq_div_mul _ _ _).symm, div_self h]; refl
id └─────┘ └──┘
src └─────┘ └──┘
typ └─────┘ └──┘
doc └──┘
762
763 @[simp] lemma tan_zero : tan 0 = 0 := by simp [tan]
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
doc └──┘
764
765 @[simp] lemma tan_neg : tan (-x) = -tan x := by simp [tan, neg_div]
id └┘ ┴ └┘ ┴ └─┘
src └┘ └┘ └─┘
typ └┘ ┴ └┘ ┴ └─┘
doc └──┘
766
767 lemma sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
768 of_real_inj.1 $ by simpa using sin_sq_add_cos_sq x
id ┴
typ ┴
769
770 lemma sin_sq_le_one : sin x ^ 2 ≤ 1 :=
id └┘ ┴
src └┘
typ └┘ ┴
771 by rw ← sin_sq_add_cos_sq x; exact le_add_of_nonneg_right' (pow_two_nonneg _)
772
773 lemma cos_sq_le_one : cos x ^ 2 ≤ 1 :=
id └┘ ┴
src └┘
typ └┘ ┴
774 by rw ← sin_sq_add_cos_sq x; exact le_add_of_nonneg_left' (pow_two_nonneg _)
775
776 lemma abs_sin_le_one : abs' (sin x) ≤ 1 :=
id └┘ ┴
src └┘
typ └┘ ┴
777 (mul_self_le_mul_self_iff (_root_.abs_nonneg (sin x)) (by exact zero_le_one)).2 $
id └┘ ┴
src └┘
typ └┘ ┴
778 by rw [← _root_.abs_mul, abs_mul_self, mul_one, ← pow_two];
779 apply sin_sq_le_one
780
781 lemma abs_cos_le_one : abs' (cos x) ≤ 1 :=
id └┘ ┴
src └┘
typ └┘ ┴
782 (mul_self_le_mul_self_iff (_root_.abs_nonneg (cos x)) (by exact zero_le_one)).2 $
id └┘ ┴
src └┘
typ └┘ ┴
783 by rw [← _root_.abs_mul, abs_mul_self, mul_one, ← pow_two];
784 apply cos_sq_le_one
785
786 lemma sin_le_one : sin x ≤ 1 :=
id └┘ ┴
src └┘
typ └┘ ┴
787 (abs_le.1 (abs_sin_le_one _)).2
788
789 lemma cos_le_one : cos x ≤ 1 :=
id └┘ ┴
src └┘
typ └┘ ┴
790 (abs_le.1 (abs_cos_le_one _)).2
791
792 lemma neg_one_le_sin : -1 ≤ sin x :=
id └┘ ┴
src └┘
typ └┘ ┴
793 (abs_le.1 (abs_sin_le_one _)).1
794
795 lemma neg_one_le_cos : -1 ≤ cos x :=
id └┘ ┴
src └┘
typ └┘ ┴
796 (abs_le.1 (abs_cos_le_one _)).1
797
798 lemma cos_two_mul : cos (2 * x) = 2 * cos x ^ 2 - 1 :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
799 by rw ← of_real_inj; simp [cos_two_mul]
800
801 lemma sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
id └┘ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ ┴ └┘ ┴ ┴ ┴
802 by rw ← of_real_inj; simp [sin_two_mul]
803
804 lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
805 of_real_inj.1 $ by simpa using cos_square x
id ┴
typ ┴
806
807 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
808 eq_sub_iff_add_eq.2 $ sin_sq_add_cos_sq _
809
810 @[simp] lemma sinh_zero : sinh 0 = 0 := by simp [sinh]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └──┘
811
812 @[simp] lemma sinh_neg : sinh (-x) = -sinh x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
813 by simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]
id └──┘
src └──┘
typ └──┘
814
815 lemma sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
816 by rw ← of_real_inj; simp [sinh_add]
817
818 @[simp] lemma cosh_zero : cosh 0 = 1 := by simp [cosh]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └──┘
819
820 @[simp] lemma cosh_neg : cosh (-x) = cosh x :=
id └┘ ┴ └┘ ┴
src └┘ └┘
typ └┘ ┴ └┘ ┴
doc └──┘
821 by simp [cosh, exp_neg]
id └──┘
src └──┘
typ └──┘
822
823 lemma cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
824 by rw ← of_real_inj; simp [cosh, cosh_add]
id └──┘
src └──┘
typ └──┘
825
826 lemma sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
827 by simp [sinh_add, sinh_neg, cosh_neg]
828
829 lemma cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘ └┘ └┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
830 by simp [cosh_add, sinh_neg, cosh_neg]
831
832 lemma tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x :=
id └┘ ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └┘
typ └┘ ┴ └┘ ┴ └┘ ┴
833 of_real_inj.1 $ by simp [tanh_eq_sinh_div_cosh]
834
835 @[simp] lemma tanh_zero : tanh 0 = 0 := by simp [tanh]
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
doc └──┘
836
837 @[simp] lemma tanh_neg : tanh (-x) = -tanh x := by simp [tanh, neg_div]
id └┘ ┴ └┘ ┴ └──┘
src └┘ └┘ └──┘
typ └┘ ┴ └┘ ┴ └──┘
doc └──┘
838
839 open is_absolute_value
840
841 /- TODO make this private and prove ∀ x -/
842 lemma add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x :=
id ┴ ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ └┘ ┴
843 calc x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩ : cau_seq ℝ abs') :
id ┴ ┴ ┴ ┴ └┘ ┴ ┴
src ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴
844 le_lim (cau_seq.le_of_exists ⟨2,
845 λ j hj, show x + (1 : ℝ) ≤ ((range j).sum (λ m, (x ^ m / m.fact : ℂ))).re,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ ┴
846 from have h₁ : (((λ m : ℕ, (x ^ m / m.fact : ℂ)) ∘ nat.succ) 0).re = x, by simp,
id ┴ ┴ ┴ ┴└┘ └┘ ┴ └─┘ └─┘ ┴ ┴
src ┴ └┘ └┘ ┴ └─┘ └─┘ ┴
typ ┴ ┴ ┴ ┴└┘ └┘ ┴ └─┘ └─┘ ┴ ┴
doc └┘ └┘
847 have h₂ : ((x : ℂ) ^ 0 / nat.fact 0).re = 1, by simp,
id ┴ ┴ └──────┘ └┘
src ┴ └──────┘ └┘
typ ┴ ┴ └──────┘ └┘
doc └──────┘
848 begin
849 rw [← nat.sub_add_cancel hj, sum_range_succ', sum_range_succ',
850 add_re, add_re, h₁, h₂, add_assoc,
851 ← @sum_hom _ _ _ _ _ _ _ complex.re
id └────────┘
src └────────┘
typ └────────┘
852 (is_add_group_hom.to_is_add_monoid_hom _)],
853 refine le_add_of_nonneg_of_le (sum_nonneg (λ m hm, _)) (le_refl _), dsimp [-nat.fact_succ],
id ┴
typ ┴
854 rw [← of_real_pow, ← of_real_nat_cast, ← of_real_div, of_real_re],
855 exact div_nonneg (pow_nonneg hx _) (nat.cast_pos.2 (nat.fact_pos _)),
856 end⟩)
st └─┘
857 ... = exp x : by rw [exp, complex.exp, ← cau_seq_re, lim_re]
id └─┘ ┴
src └─┘
typ └─┘ ┴
st ┴
858
859 lemma one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x :=
id ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ └┘ ┴
860 by linarith [add_one_le_exp_of_nonneg hx]
861
862 lemma exp_pos (x : ℝ) : 0 < exp x :=
id ┴ └┘ ┴
src ┴ └┘
typ ┴ └┘ ┴
863 (le_total 0 x).elim (lt_of_lt_of_le zero_lt_one ∘ one_le_exp)
id ┴
typ ┴
864 (λ h, by rw [← neg_neg x, real.exp_neg];
865 exact inv_pos (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h))))
866
867 @[simp] lemma abs_exp (x : ℝ) : abs' (exp x) = exp x :=
id ┴ └┘ ┴ └┘ ┴
src ┴ └┘ └┘
typ ┴ └┘ ┴ └┘ ┴
doc └──┘
868 abs_of_pos (exp_pos _)
869
870 lemma exp_strict_mono : strict_mono exp :=
id └┘
src └┘
typ └┘
871 λ x y h, by rw [← sub_add_cancel y x, real.exp_add];
id ┴ ┴
typ ┴ ┴
872 exact (lt_mul_iff_one_lt_left (exp_pos _)).2
873 (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
874
875 lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴
src ┴ └┘ ┴ ┴ └──┘ └──┘ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴
876
877 lemma exp_le_exp {x y : ℝ} : exp x ≤ exp y ↔ x ≤ y := exp_strict_mono.le_iff_le
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴
src ┴ └┘ └┘ ┴ └──┘ └──┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴
878
879 lemma exp_injective : function.injective exp := exp_strict_mono.injective
id └┘ └┘ └┘ └┘ └┘
src └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘
880
881 @[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 :=
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
doc └──┘
882 by rw [← exp_zero, exp_injective.eq_iff]
883
884 lemma one_lt_exp_iff {x : ℝ} : 1 < exp x ↔ 0 < x :=
id ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴
885 by rw [← exp_zero, exp_lt_exp]
886
887 lemma exp_lt_one_iff {x : ℝ} : exp x < 1 ↔ x < 0 :=
id ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴
888 by rw [← exp_zero, exp_lt_exp]
889
890 end real
891
892 namespace complex
893
894 lemma sum_div_fact_le {α : Type*} [discrete_linear_ordered_field α] (n j : ℕ) (hn : 0 < n) :
id └┘ └──┘ └──┘ └──┘ └──┘ ┴ ┴ ┴ ┴
src └┘ └──┘ └──┘ └──┘ └──┘ ┴ ┴
typ └┘ └──┘ └──┘ └──┘ └──┘ ┴ ┴ ┴ ┴
895 (sum (filter (λ k, n ≤ k) (range j)) (λ m : ℕ, (1 / m.fact : α))) ≤ n.succ * (n.fact * n)⁻¹ :=
id ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└─┘ ┴┴ └┘ ┴
src ┴ └──┘ └─┘ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└─┘ ┴┴ └┘ ┴
doc └──┘ ┴ └┘
896 calc (filter (λ k, n ≤ k) (range j)).sum (λ m : ℕ, (1 / m.fact : α))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
897 = (range (j - n)).sum (λ m, 1 / (m + n).fact) :
id ┴ ┴ ┴ ┴ ┴ └┘
src └┘
typ ┴ ┴ ┴ ┴ ┴ └┘
doc └┘
898 sum_bij (λ m _, m - n)
id ┴ ┴ ┴
typ ┴ ┴ ┴
899 (λ m hm, mem_range.2 $ (nat.sub_lt_sub_right_iff (by simp at hm; tauto)).2
id ┴
typ ┴
900 (by simp at hm; tauto))
901 (λ m hm, by rw nat.sub_add_cancel; simp at *; tauto)
id ┴
typ ┴
902 (λ a₁ a₂ ha₁ ha₂ h,
id └┘ └┘
typ └┘ └┘
903 by rwa [nat.sub_eq_iff_eq_add, ← nat.sub_add_comm, eq_comm, nat.sub_eq_iff_eq_add, add_right_inj, eq_comm] at h;
904 simp at *; tauto)
905 (λ b hb, ⟨b + n, mem_filter.2 ⟨mem_range.2 $ nat.add_lt_of_lt_sub_right (mem_range.1 hb), nat.le_add_left _ _⟩,
id ┴ ┴ ┴
typ ┴ ┴ ┴
906 by rw nat.add_sub_cancel⟩)
907 ... ≤ (range (j - n)).sum (λ m, (nat.fact n * n.succ ^ m)⁻¹) :
id ┴ ┴ ┴ └──────┘ ┴ ┴└───┘ ┴
src └──────┘ └───┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴└───┘ ┴
doc └──────┘
908 begin
909 refine sum_le_sum (assume m n, _),
id ┴
typ ┴
910 rw [one_div_eq_inv, inv_le_inv],
911 { rw [← nat.cast_pow, ← nat.cast_mul, nat.cast_le, add_comm],
912 exact nat.fact_mul_pow_le_fact },
st └┘
913 { exact nat.cast_pos.2 (nat.fact_pos _) },
st └┘
914 { exact mul_pos (nat.cast_pos.2 (nat.fact_pos _)) (pow_pos (nat.cast_pos.2 (nat.succ_pos _)) _) },
st └┘
915 end
st └─┘
916 ... = (nat.fact n)⁻¹ * (range (j - n)).sum (λ m, n.succ⁻¹ ^ m) :
id └──────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └──────┘ └───┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └──────┘
917 by simp [mul_inv', mul_sum.symm, sum_mul.symm, -nat.fact_succ, mul_comm, inv_pow']
918 ... = (n.succ - n.succ * n.succ⁻¹ ^ (j - n)) / (n.fact * n) :
id ┴└───┘ ┴└───┘ ┴└───┘ ┴ ┴ ┴└───┘ ┴
src └───┘ └───┘ └───┘ └───┘
typ ┴└───┘ ┴└───┘ ┴└───┘ ┴ ┴ ┴└───┘ ┴
doc └───┘
919 have h₁ : (n.succ : α) ≠ 1, from @nat.cast_one α _ _ ▸ mt nat.cast_inj.1
id ┴└───┘ ┴ ┴
src └───┘
typ ┴└───┘ ┴ ┴
920 (mt nat.succ_inj (nat.pos_iff_ne_zero.1 hn)),
921 have h₂ : (n.succ : α) ≠ 0, from nat.cast_ne_zero.2 (nat.succ_ne_zero _),
id ┴└───┘ ┴
src └───┘
typ ┴└───┘ ┴
922 have h₃ : (n.fact * n : α) ≠ 0, from mul_ne_zero (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 (nat.fact_pos _)))
id ┴└───┘ ┴ ┴
src └───┘
typ ┴└───┘ ┴ ┴
doc └───┘
923 (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 hn)),
924 have h₄ : (n.succ - 1 : α) = n, by simp,
id ┴└───┘ ┴ ┴
src └───┘
typ ┴└───┘ ┴ ┴
925 by rw [← geom_series_def, geom_sum_inv h₁ h₂, eq_div_iff_mul_eq _ _ h₃, mul_comm _ (n.fact * n : α),
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
doc └────┘
926 ← mul_assoc (n.fact⁻¹ : α), ← mul_inv', h₄, ← mul_assoc (n.fact * n : α),
id └────┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘
typ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
927 mul_comm (n : α) n.fact, mul_inv_cancel h₃];
id ┴ └────┘
src └────┘
typ ┴ └────┘
doc └────┘
928 simp [mul_add, add_mul, mul_assoc, mul_comm]
929 ... ≤ n.succ / (n.fact * n) :
id ┴└───┘ ┴└───┘ ┴
src └───┘ └───┘
typ ┴└───┘ ┴└───┘ ┴
doc └───┘
930 begin
931 refine (div_le_div_right (mul_pos _ _)).2 _,
932 exact nat.cast_pos.2 (nat.fact_pos _),
933 exact nat.cast_pos.2 hn,
934 exact sub_le_self _ (mul_nonneg (nat.cast_nonneg _) (pow_nonneg (inv_nonneg.2 (nat.cast_nonneg _)) _))
935 end
st └─┘
936
937 lemma exp_bound {x : ℂ} (hx : abs x ≤ 1) {n : ℕ} (hn : 0 < n) :
id ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴
938 abs (exp x - (range n).sum (λ m, x ^ m / m.fact)) ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹) :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ └┘ └┘ ┴ ┴ ┴┴ └─┘ ┴└┘ └┘ ┴
src └┘ ┴ └┘ └┘ └┘ ┴ └─┘ └┘ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ └┘ └┘ ┴ ┴ ┴┴ └─┘ ┴└┘ └┘ ┴
doc └┘ └┘ └┘ └┘
939 begin
940 rw [← lim_const ((range n).sum _), exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_abs],
941 refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),
id ┴ ┴ └┘
typ ┴ ┴ └┘
942 show abs ((range j).sum (λ m, x ^ m / m.fact) - (range n).sum (λ m, x ^ m / m.fact))
id ┴ ┴ ┴
typ ┴ ┴ ┴
943 ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹),
id └─┘ ┴ └────┘ └────┘ ┴
src └─┘ └────┘ └────┘
typ └─┘ ┴ └────┘ └────┘ ┴
doc └────┘
944 rw sum_range_sub_sum_range hj,
id └┘
typ └┘
945 exact calc abs (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (x ^ m / m.fact : ℂ)))
id ┴
typ ┴
946 = abs (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (x ^ n * (x ^ (m - n) / m.fact) : ℂ))) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
947 congr_arg abs (sum_congr rfl (λ m hm, by rw [← mul_div_assoc, ← pow_add, nat.add_sub_cancel']; simp at hm; tauto))
id ┴
typ ┴
948 ... ≤ sum (filter (λ k, n ≤ k) (range j)) (λ m, abs (x ^ n * (_ / m.fact))) : abv_sum_le_sum_abv _ _
id ┴ ┴
typ ┴ ┴
949 ... ≤ sum (filter (λ k, n ≤ k) (range j)) (λ m, abs x ^ n * (1 / m.fact)) :
id ┴ ┴
typ ┴ ┴
950 begin
951 refine sum_le_sum (λ m hm, _),
id ┴
typ ┴
952 rw [abs_mul, abv_pow abs, abs_div, abs_cast_nat],
id └─┘
src └─┘
typ └─┘
953 refine mul_le_mul_of_nonneg_left ((div_le_div_right _).2 _) _,
954 exact nat.cast_pos.2 (nat.fact_pos _),
955 rw abv_pow abs,
id └─┘
src └─┘
typ └─┘
956 exact (pow_le_one _ (abs_nonneg _) hx),
957 exact pow_nonneg (abs_nonneg _) _
958 end
st └─┘
959 ... = abs x ^ n * (((range j).filter (λ k, n ≤ k)).sum (λ m : ℕ, (1 / m.fact : ℝ))) :
id ┴
typ ┴
960 by simp [abs_mul, abv_pow abs, abs_div, mul_sum.symm]
id └─┘
src └─┘
typ └─┘
961 ... ≤ abs x ^ n * (n.succ * (n.fact * n)⁻¹) :
id └────┘ └────┘
src └────┘ └────┘
typ └────┘ └────┘
doc └────┘
962 mul_le_mul_of_nonneg_left (sum_div_fact_le _ _ hn) (pow_nonneg (abs_nonneg _) _)
963 end
st └─┘
964
965 lemma abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) :
id ┴ └┘ ┴
src ┴ └┘
typ ┴ └┘ ┴
966 abs (exp x - 1) ≤ 2 * abs x :=
id └┘ ┴ ┴ └┘ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ └┘ ┴
967 calc abs (exp x - 1) = abs (exp x - (range 1).sum (λ m, x ^ m / m.fact)) :
id ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ └┘ └┘ └──┘
typ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
968 by simp [sum_range_succ]
969 ... ≤ abs x ^ 1 * ((nat.succ 1) * (nat.fact 1 * (1 : ℕ))⁻¹) :
id └─┘ ┴ └──────┘ └──────┘ ┴
src └─┘ └──────┘ └──────┘ ┴
typ └─┘ ┴ └──────┘ └──────┘ ┴
doc └──────┘
970 exp_bound hx dec_trivial
971 ... = 2 * abs x : by simp [two_mul, mul_two, mul_add, mul_comm]
id └─┘ ┴
src └─┘
typ └─┘ ┴
972
973 lemma abs_exp_sub_one_sub_id_le {x : ℂ} (hx : abs x ≤ 1) :
id ┴ └┘ ┴
src ┴ └┘
typ ┴ └┘ ┴
974 abs (exp x - 1 - x) ≤ (abs x)^2 :=
id └┘ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └┘ ┴
975 calc abs (exp x - 1 - x) = abs (exp x - (range 2).sum (λ m, x ^ m / m.fact)) :
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └┘ ┴ └──┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
976 by simp [sum_range_succ]
977 ... ≤ (abs x)^2 * (nat.succ 2 * (nat.fact 2 * (2 : ℕ))⁻¹) :
id └─┘ ┴ └──────┘ └──────┘ ┴
src └─┘ └──────┘ └──────┘ ┴
typ └─┘ ┴ └──────┘ └──────┘ ┴
doc └──────┘
978 exp_bound hx dec_trivial
979 ... ≤ (abs x)^2 * 1 :
id └─┘ ┴
src └─┘
typ └─┘ ┴
980 mul_le_mul_of_nonneg_left (by norm_num) (pow_two_nonneg (abs x))
id └─┘ ┴
src └─┘
typ └─┘ ┴
981 ... = (abs x)^2 :
id └─┘ ┴
src └─┘
typ └─┘ ┴
982 by rw [mul_one]
st ┴
983
984 end complex
985
986 namespace real
987
988 open complex finset
989
990 lemma cos_bound {x : ℝ} (hx : abs' x ≤ 1) : abs' (cos x - (1 - x ^ 2 / 2)) ≤ abs' x ^ 4 * (5 / 96) :=
id ┴ ┴ └┘ ┴ ┴ ┴
src ┴ └┘
typ ┴ ┴ └┘ ┴ ┴ ┴
991 calc abs' (cos x - (1 - x ^ 2 / 2)) = abs (complex.cos x - (1 - x ^ 2 / 2)) :
id ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘ └┘
typ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴
992 by rw ← abs_of_real; simp [of_real_bit0, of_real_one, of_real_inv]
993 ... = abs ((complex.exp (x * I) + complex.exp (-x * I) - (2 - x ^ 2)) / 2) :
id └─┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └─┘ └─────────┘ ┴ └─────────┘ ┴
typ └─┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴
994 by simp [complex.cos, sub_div, add_div, neg_div, div_self (@two_ne_zero' ℂ _ _ _)]
id └─────────┘
src └─────────┘
typ └─────────┘
995 ... = abs (((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact)) +
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
996 ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)))) / 2) :
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─────────┘ ┴ ┴ └───┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
997 congr_arg abs (congr_arg (λ x : ℂ, x / 2) begin
id └─┘ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴
998 simp only [sum_range_succ],
999 simp [pow_succ],
1000 apply complex.ext; simp [div_eq_mul_inv, norm_sq]; ring
id └─────┘
src └─────┘
typ └─────┘
1001 end)
st └─┘
1002 ... ≤ abs ((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact)) / 2) +
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1003 abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)) / 2) :
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1004 by rw add_div; exact abs_add _ _
1005 ... = (abs ((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact))) / 2 +
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1006 abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact))) / 2) :
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1007 by simp [complex.abs_div]
1008 ... ≤ ((complex.abs (x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2 +
id └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
src └─────────┘ ┴ └──────┘ └──────┘ ┴
typ └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
doc └──────┘
1009 (complex.abs (-x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2) :
id └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
src └─────────┘ ┴ └──────┘ └──────┘ ┴
typ └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
doc └──────┘
1010 add_le_add ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1011 ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1012 ... ≤ abs' x ^ 4 * (5 / 96) : by norm_num; simp [mul_assoc, mul_comm, mul_left_comm, mul_div_assoc]
id ┴
typ ┴
1013
1014 lemma sin_bound {x : ℝ} (hx : abs' x ≤ 1) : abs' (sin x - (x - x ^ 3 / 6)) ≤ abs' x ^ 4 * (5 / 96) :=
id ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └┘
typ ┴ └┘ ┴ ┴ ┴ ┴
1015 calc abs' (sin x - (x - x ^ 3 / 6)) = abs (complex.sin x - (x - x ^ 3 / 6)) :
id ┴ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘ └┘
typ ┴ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
1016 by rw ← abs_of_real; simp [of_real_bit0, of_real_one, of_real_inv]
1017 ... = abs (((complex.exp (-x * I) - complex.exp (x * I)) * I - (2 * x - x ^ 3 / 3)) / 2) :
id └─┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └─────────┘ ┴ └─────────┘ ┴ ┴
typ └─┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴
1018 by simp [complex.sin, sub_div, add_div, neg_div, mul_div_cancel_left _ (@two_ne_zero' ℂ _ _ _),
id └─────────┘
src └─────────┘
typ └─────────┘
1019 div_div_eq_div_mul, show (3 : ℂ) * 2 = 6, by norm_num]
1020 ... = abs ((((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)) -
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1021 (complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact))) * I) / 2) :
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └─────────┘ ┴ ┴ └───┘ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └───┘
1022 congr_arg abs (congr_arg (λ x : ℂ, x / 2) begin
id └─┘ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴
1023 simp only [sum_range_succ],
1024 simp [pow_succ],
1025 apply complex.ext; simp [div_eq_mul_inv, norm_sq]; ring
id └─────┘
src └─────┘
typ └─────┘
1026 end)
st └─┘
1027 ... ≤ abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact)) * I / 2) +
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └─┘ └─────────┘ ┴ ┴ └───┘ ┴
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └───┘
1028 abs (-((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact)) * I) / 2) :
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └─┘ └─────────┘ ┴ ┴ └───┘ ┴
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └───┘
1029 by rw [sub_mul, sub_eq_add_neg, add_div]; exact abs_add _ _
1030 ... = (abs ((complex.exp (x * I) - (range 4).sum (λ m, (x * I) ^ m / m.fact))) / 2 +
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1031 abs ((complex.exp (-x * I) - (range 4).sum (λ m, (-x * I) ^ m / m.fact))) / 2) :
id └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
src └─┘ └─────────┘ ┴ ┴ └───┘
typ └─┘ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘
doc └───┘
1032 by simp [complex.abs_div, complex.abs_mul]
1033 ... ≤ ((complex.abs (x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2 +
id └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
src └─────────┘ ┴ └──────┘ └──────┘ ┴
typ └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
doc └──────┘
1034 (complex.abs (-x * I) ^ 4 * (nat.succ 4 * (nat.fact 4 * (4 : ℕ))⁻¹)) / 2) :
id └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
src └─────────┘ ┴ └──────┘ └──────┘ ┴
typ └─────────┘ ┴ ┴ └──────┘ └──────┘ ┴
doc └──────┘
1035 add_le_add ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1036 ((div_le_div_right (by norm_num)).2 (exp_bound (by simpa) dec_trivial))
1037 ... ≤ abs' x ^ 4 * (5 / 96) : by norm_num; simp [mul_assoc, mul_comm, mul_left_comm, mul_div_assoc]
id ┴
typ ┴
1038
1039 lemma cos_pos_of_le_one {x : ℝ} (hx : abs' x ≤ 1) : 0 < cos x :=
id ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ └┘ ┴
1040 calc 0 < (1 - x ^ 2 / 2) - abs' x ^ 4 * (5 / 96) :
id ┴ ┴
typ ┴ ┴
1041 sub_pos.2 $ lt_sub_iff_add_lt.2
1042 (calc abs' x ^ 4 * (5 / 96) + x ^ 2 / 2
id ┴ ┴
typ ┴ ┴
1043 ≤ 1 * (5 / 96) + 1 / 2 :
1044 add_le_add
1045 (mul_le_mul_of_nonneg_right (pow_le_one _ (abs_nonneg _) hx) (by norm_num))
1046 ((div_le_div_right (by norm_num)).2 (by rw [pow_two, ← abs_mul_self, _root_.abs_mul];
1047 exact mul_le_one hx (abs_nonneg _) hx))
1048 ... < 1 : by norm_num)
1049 ... ≤ cos x : sub_le.1 (abs_sub_le_iff.1 (cos_bound hx)).2
id └─┘ ┴
src └─┘
typ └─┘ ┴
1050
1051 lemma sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < sin x :=
id ┴ ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ └┘ ┴
1052 calc 0 < x - x ^ 3 / 6 - abs' x ^ 4 * (5 / 96) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
1053 sub_pos.2 $ lt_sub_iff_add_lt.2
1054 (calc abs' x ^ 4 * (5 / 96) + x ^ 3 / 6
id ┴ ┴
typ ┴ ┴
1055 ≤ x * (5 / 96) + x / 6 :
id ┴
typ ┴
1056 add_le_add
1057 (mul_le_mul_of_nonneg_right
1058 (calc abs' x ^ 4 ≤ abs' x ^ 1 : pow_le_pow_of_le_one (abs_nonneg _)
id ┴ ┴
typ ┴ ┴
1059 (by rwa _root_.abs_of_nonneg (le_of_lt hx0))
1060 dec_trivial
1061 ... = x : by simp [_root_.abs_of_nonneg (le_of_lt (hx0))]) (by norm_num))
id ┴
typ ┴
1062 ((div_le_div_right (by norm_num)).2
1063 (calc x ^ 3 ≤ x ^ 1 : pow_le_pow_of_le_one (le_of_lt hx0) hx dec_trivial
id ┴ ┴
typ ┴ ┴
1064 ... = x : pow_one _))
id ┴
typ ┴
1065 ... < x : by linarith)
id ┴
typ ┴
1066 ... ≤ sin x : sub_le.1 (abs_sub_le_iff.1 (sin_bound
id └─┘ ┴
src └─┘
typ └─┘ ┴
1067 (by rwa [_root_.abs_of_nonneg (le_of_lt hx0)]))).2
1068
1069 lemma sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) : 0 < sin x :=
id ┴ ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ └┘ ┴
1070 have x / 2 ≤ 1, from div_le_of_le_mul (by norm_num) (by simpa),
id ┴
typ ┴
1071 calc 0 < 2 * sin (x / 2) * cos (x / 2) :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
1072 mul_pos (mul_pos (by norm_num) (sin_pos_of_pos_of_le_one (half_pos hx0) this))
1073 (cos_pos_of_le_one (by rwa [_root_.abs_of_nonneg (le_of_lt (half_pos hx0))]))
1074 ... = sin x : by rw [← sin_two_mul, two_mul, add_halves]
id └─┘ ┴
src └─┘
typ └─┘ ┴
st ┴
1075
1076 lemma cos_one_le : cos 1 ≤ 2 / 3 :=
id └┘
src └┘
typ └┘
1077 calc cos 1 ≤ abs' (1 : ℝ) ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) :
id ┴ ┴
src ┴ ┴
typ ┴ ┴
1078 sub_le_iff_le_add.1 (abs_sub_le_iff.1 (cos_bound (by simp))).1
1079 ... ≤ 2 / 3 : by norm_num
1080
1081 lemma cos_one_pos : 0 < cos 1 := cos_pos_of_le_one (by simp)
id └┘
src └┘
typ └┘
1082
1083 lemma cos_two_neg : cos 2 < 0 :=
id └┘
src └┘
typ └┘
1084 calc cos 2 = cos (2 * 1) : congr_arg cos (mul_one _).symm
id └┘ └┘
src └┘ └┘
typ └┘ └┘
1085 ... = _ : real.cos_two_mul 1
1086 ... ≤ 2 * (2 / 3) ^ 2 - 1 :
1087 sub_le_sub_right (mul_le_mul_of_nonneg_left
1088 (by rw [pow_two, pow_two]; exact
1089 mul_self_le_mul_self (le_of_lt cos_one_pos)
1090 cos_one_le)
1091 (by norm_num)) _
1092 ... < 0 : by norm_num
1093
1094 end real
1095
1096 namespace complex
1097
1098 lemma abs_cos_add_sin_mul_I (x : ℝ) : abs (cos x + sin x * I) = 1 :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴
src ┴ └┘ └┘ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴
1099 have _ := real.sin_sq_add_cos_sq x,
id ┴
typ ┴
1100 by simp [abs, norm_sq, pow_two, *, sin_of_real_re, cos_of_real_re, mul_re] at *
id └─┘ └─────┘
src └─┘ └─────┘
typ └─┘ └─────┘
1101
1102 lemma abs_exp_eq_iff_re_eq {x y : ℂ} : abs (exp x) = abs (exp y) ↔ x.re = y.re :=
id ┴ └┘ └┘ ┴ ┴ └┘ ┴└─┘ ┴└┘
src ┴ └┘ └┘ ┴ └┘ └─┘ └┘
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴└─┘ ┴└┘
1103 by rw [exp_eq_exp_re_mul_sin_add_cos, exp_eq_exp_re_mul_sin_add_cos y,
1104 abs_mul, abs_mul, abs_cos_add_sin_mul_I, abs_cos_add_sin_mul_I,
1105 ← of_real_exp, ← of_real_exp, abs_of_nonneg (le_of_lt (real.exp_pos _)),
1106 abs_of_nonneg (le_of_lt (real.exp_pos _)), mul_one, mul_one];
1107 exact ⟨λ h, real.exp_injective h, congr_arg _⟩
id └────────────────┘
src └────────────────┘
typ └────────────────┘
1108
1109 @[simp] lemma abs_exp_of_real (x : ℝ) : abs (exp x) = real.exp x :=
id ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴
src ┴ └┘ └┘ ┴ └┘ ┴
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
1110 by rw [← of_real_exp]; exact abs_of_nonneg (le_of_lt (real.exp_pos _))
1111
1112 end complex